Summary
Synchronous languages rely on formal methods to ease the development of applications in an efficient and reusable way. Formal methods have been advocated as a means of increasing the reliability of systems, especially those which are safety or business critical. It is still difficult to develop automatic specification and verification tools due to limitations like state explosion, undecidability, etc... In this work, we design a new specification model based on a reactive synchronous approach. Then, we benefit from a formal framework well suited to perform compilation and formal validation of systems. In practice, we design and implement a special purpose language (le ) and its two semantics : the behavioral semantics helps us to define a program by the set of its behaviors and avoid ambiguousness in programs’ interpretation; the execution equational semantics allows the modular compilation of programs into software and hardware targets (C code, Vhdl code, Fpga synthesis, Verification tools). Our approach is pertinent considering the two main requirements of critical realistic applications : the modular compilation allows us to deal with large systems, the model-driven approach provides us with formal validation.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
André, C., Boufaïed, H., Dissoubray, S.: Synccharts: un modéle graphique synchrone pour systéme réactifs complexes. In: Real-Time Systems (RTS 1998), Paris, France, January 1998, pp. 175–196. Teknea (1998)
Berry, G.: The Constructive Semantics of Pure Esterel. Draft Book (1996), http://www.esterel-technologies.com
Berry, G.: The Foundations of Esterel. In: Plotkin, G., Stearling, C., Tofte, M. (eds.) Proof, Language, and Interaction, Essays in Honor of Robin Milner. MIT Press, Cambridge (2000)
Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an OpenSource Tool for Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002)
Cousot, P., Cousot, R.: On Abstraction in Software Verification. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 37, 56. Springer, Heidelberg (2002)
Edwards, S.A.: Compiling esterel into sequential code. In: Proceedings of the 7th International Workshop on Hardware/Software Codesign (CODES 1999), Rome, Italy, May 1999, pp. 147–151 (1999)
Edwards, S.A., Lee, E.A.: The semantics and execution of a synchronous block-diagram language. Science of Computer Programming 48(1), 21–42 (2003)
Halbwachs, N.: Synchronous Programming of Reactive Systems. Kluwer Academic, Dordrecht (1993)
Halbwachs, N., Lagnier, F., Raymond, P.: Synchronous observers and the verification of reactive systems. In: Nivat, M., Rattray, C., Rus, T., Scollo, G. (eds.) Third Int. Conf. on Algebraic Methodology and Software Technology, AMAST 1993, Workshops in Computing, Twente, June 1993. Springer, Heidelberg (1993)
Harel, D., Pnueli, A.: On the development of reactive systems. In: NATO, Advanced Study institute on Logics and Models for Verification and Specification of Concurrent Systems. Springer, Heidelberg (1985)
Huizing, C., Gerth, R.: Semantics of reactive systems in abstract time. In: de Roever, W.P., Rozenberg, G. (eds.) Real Time: Theory in Practice, Proc. of REX workshop, June 1991. LNCS, pp. 291–314. Springer, Heidelberg (1991)
Clarke Jr., E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)
Lublinerman, R., Tripakis, S.: Modularity vs. reusability: Code generation from synchronous block diagrams. In: Design, Automation and Test in Europe (DATE 2008) (2008)
Potop-Butucaru, D., De Simone, R.: Optimizations for Faster Execution of Esterel Programs. In: Gupta, R., LeGuernic, P., Shukla, S., Talpin, J.-P. (eds.) Formal Methods and Models for System Design, Kluwer, Dordrecht (2004)
Ressouche, A., Gaffé, D., Roy, V.: Modular compilation of a synchronous language. Research Report 6424, INRIA (January 2008), https://hal.inria.fr/inria-00213472
K. Schneider, J. Brand, E. Vecchié. Modular compilation of synchronous programs. In From Model-Driven Design to Resource Management for Distributed Embedded Systems, volume 225 of IFIP International Federation for Information Processing, pages 75–84. Springer Boston, January 2006.
Esterel Technologies. Esterel studio suite, http://www.estereltechnologies.com
Kirkpatrick, T.I., Clark, N.R.: Pert and an aid to logic design. IBM Journal of Research and Develepment, 135–141 (March 1966)
Weil, D., Bertin, V., Closse, E., Poize, M., Venier, P., Pulou, J.: Efficient compilation of esterel for real-time embedded systems. In: Proceedings of the 2000 International Conference on Compilers, Architecture, and Synthesis for Embedded Systems, San Jose, California, United States, November 2000, pp. 2–8 (2000)
Zeng, J., Edwards, S.A.: Separate compilation for synchronous modules. In: Yang, L.T., Zhou, X.-s., Zhao, W., Wu, Z., Zhu, Y., Lin, M. (eds.) ICESS 2005. LNCS, vol. 3820, pp. 129–140. Springer, Heidelberg (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Ressouche, A., Gaffé, D., Roy, V. (2008). Modular Compilation of a Synchronous Language. In: Lee, R. (eds) Software Engineering Research, Management and Applications. Studies in Computational Intelligence, vol 150. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70561-1_12
Download citation
DOI: https://doi.org/10.1007/978-3-540-70561-1_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-70774-5
Online ISBN: 978-3-540-70561-1
eBook Packages: EngineeringEngineering (R0)