Abstract
Synchronous programming languages like Esterel are becoming more and more popular for the design of multi-threaded reactive systems. We have embedded a variant of the Esterel language in the interactive theorem prover HOL so that we can formally reason about programs of the language and — at a meta level — about the language itself Based on a separation of the control and data flow of the programs, we have defined a new translation to equation systems. Our new translation is simpler than state-of-the-art translations, and it does not suffer from the schizophrenia problems of parallel statements. Furthermore, we have proved the correctness of our translation with HOL, so that HOL can be used for formal synthesis.
The original version of this chapter was revised: The copyright line was incorrect. This has been corrected. The Erratum to this chapter is available at DOI: 10.1007/978-0-387-35409-5_23
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Esterel Web. http://www.esterel.org.
Simulog. http://www.simulog.fr.
Cadence Design Systems,Inc. http://www.cadence.com.
ECL Homepage. http://www-cad.eecs.berkeley.edu/
Jester Homepage. http://www.parades.rm.cnr.it/projects/jester/jester.html.
G. Berry. The foundations of Esterel. In G. Plotkin, C. Stirling, and M. Tofte, editors, Proof Language and Interaction: Essays in Honour of Robin Milner. MIT Press, 1998.
G. Berry. The Esterel v591 language primer. http://www.esterel.org, June 2000.
N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The synchronous dataflow programming language LUSTRE. Proc. of the IEEE, 79 (9): 1305–1320, 1991.
P. Le Guernic, T. Gauthier, M. Le Borgne, and C. Le Maire. Programming real-time applications with SIGNAL. IEEE, 79 (9): 1321–1336, 1991.
D. Harel. Statecharts: A visual formalism for complex systems. Science of Computing, pp. 231–274, 1987.
Ch. Andre. Synccharts: A visual representation of reactive behaviors. research report tr95–52, University of Nice, Sophia Antipolis, 1995.
G. Berry. The constructive semantics of pure Esterel, July 1999.
J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic Model Checking: 1020 States and Beyond. IEEE Symposium on Logic in Computer Science, pp. 1–33, Washington, June 1990. IEEE Computer Society Press.
M.J.C. Gordon and T.F. Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993.
K.M. Chandry and J. Misra. Parallel Program Design: A Foundation. Addison-Wesley, 1988.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 IFIP International Federation for Information Processing
About this chapter
Cite this chapter
Schneider, K. (2001). A Verified Hardware Synthesis of Esterel Programs. In: Kleinjohann, B. (eds) Architecture and Design of Distributed Embedded Systems. DIPES 2000. IFIP — The International Federation for Information Processing, vol 61. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35409-5_20
Download citation
DOI: https://doi.org/10.1007/978-0-387-35409-5_20
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-4535-1
Online ISBN: 978-0-387-35409-5
eBook Packages: Springer Book Archive