Document Open Access Logo

Towards a Coq-verified Chain of Esterel Semantics

Authors Lionel Rieg , Gérard Berry

PDF
Thumbnail PDF

File

LITES.10.1.2.pdf
  • Filesize: 1.44 MB
  • 54 pages

Document Identifiers

Author Details

Lionel Rieg
  • Université Grenoble Alpes, CNRS, Grenoble INP - UGA, VERIMAG, Grenoble, France
  • Collège de France, Paris, France
Gérard Berry
  • Collège de France, Paris, France

Cite As Get BibTex

Lionel Rieg and Gérard Berry. Towards a Coq-verified Chain of Esterel Semantics. In LITES, Volume 10, Issue 1 (2025). Leibniz Transactions on Embedded Systems, Volume 10, Issue 1, pp. 2:1-2:54, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LITES.10.1.2

Abstract

This article focuses on formally specifying and verifying the chain of formal semantics of the Esterel synchronous programming language using the Coq proof assistant. In particular, in addition to the standard logical (LBS) semantics, constructive semantics (CBS) and constructive state semantics (CSS), we introduce a novel microstep semantics that gets rid of the Must/Can potential function pair of the constructive semantics and can be viewed as an abstract version of Esterel’s circuit semantics used by compilers to generate software code and hardware designs. The article also comes with formal proofs in Coq of the equivalence between the CBS and CSS semantics and of the refinement of the CSS by the microstep semantics, except for the loop construct of Esterel.

Subject Classification

ACM Subject Classification
  • Theory of computation → Operational semantics
  • Hardware → Theorem proving and SAT solving
  • Security and privacy → Logic and verification
  • Computer systems organization → Real-time languages
Keywords
  • Esterel programming language
  • formal verification
  • Coq proof assistant

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

Supplementary Materials

References

  1. Charles André. Representation and analysis of reactive behaviors: a synchronous approach. In Proc CESA'96, IEEE-SMC, Lille, France, 1996. URL: https://www-sop.inria.fr/members/Charles.Andre/CA%20Publis/Cesa96/SyncCharts_Cesa96.pdf.
  2. Gérard Berry. The Esterel language primer, version v5_91. Technical report, Ecole des mines de Paris and Inria, June 2000. URL: https://www.college-de-france.fr/media/gerard-berry/UPL8106359781114103786_Esterelv5_primer.pdf.
  3. Gérard Berry. The foundations of Esterel. In Proof, Language and Interaction: Essays in Honour of Robin Milner. MIT Press, 2000. URL: ftp://ftp-sop.inria.fr/meije/esterel/papers/foundations.pdf.
  4. Gérard Berry. The Constructive Semantics of Pure Esterel - Draft Version 3, 2002. URL: https://hal.science/hal-04963343.
  5. Gérard Berry, Amar Bouali, Robert de Simone, Xavier Fornari, Emmanuel Ledinot, , and Éric Nassor. Esterel: a formal method applied to avionic software development. Science of Computer Programming, 36:5-25, 2000. URL: https://doi.org/10.1016/S0167-6423(99)00015-5.
  6. Gérard Berry and Laurent Cosserat. The ESTEREL synchronous programming language and its mathematical semantics. In S. Brookes and G. Winskel, editors, Seminar on Concurrency, pages 389-448. Springer Verlag Lecture Notes in Computer Science 197, 1984. URL: https://doi.org/10.1007/3-540-15670-4_19.
  7. Gérard Berry and Georges Gonthier. The Esterel synchronous programming language: Design, semantics, implementation. Science Of Computer Programming, 19(2):87-152, 1992. URL: https://doi.org/10.1016/0167-6423(92)90005-V.
  8. Gérard Berry, Michael Kishinevsky, and Satnam Singh. System level design and verification using a synchronous language. In 2003 International Conference on Computer-Aided Design, ICCAD 2003, San Jose, CA, USA, November 9-13, 2003, pages 433-440. IEEE Computer Society / ACM, 2003. URL: https://doi.org/10.1109/ICCAD.2003.1257813.
  9. Gérard Berry, Sabie Moisan, and Jean-Paul Rigault. Towards a synchronous and semantically sound high level language for real-time applications. In IEEE Real Time Systems Symposium, pages 30-40. IEEE Catalog 83 CH 1941-4, 1983. Google Scholar
  10. Gérard Berry and Manuel Serrano. Hiphop.js: (a)synchronous reactive web programming. In Alastair F. Donaldson and Emina Torlak, editors, Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, June 15-20, 2020, pages 533-545. ACM, 2020. URL: https://doi.org/10.1145/3385412.3385984.
  11. Gérard Berry and Ravi Sethi. From regular expressions to deterministic automata. Theoretical computer science, 48:117-126, 1986. URL: https://doi.org/10.1016/0304-3975(86)90088-5.
  12. Timothy Bourke, Lélio Brun, Pierre-Évariste Dagand, Xavier Leroy, Marc Pouzet, and Lionel Rieg. A formally verified compiler for Lustre. In PLDI 2017: Programming Language Design and Implementation, pages 586-601. ACM, 2017. URL: https://doi.org/10.1145/3062341.3062358.
  13. Frédéric Boussinot. Reactive C: an extension of C to program reactive systems. Softw. Pract. Exp., 21(4):401-428, 1991. URL: https://doi.org/10.1002/spe.4380210406.
  14. Janusz A. Brozowski. Derivatives of regular expressions. Journal of the ACM, 11(4):481-494, 1964. URL: https://doi.org/10.1145/321239.321249.
  15. Randal E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, 100(8):677-691, 1986/8. URL: https://doi.org/10.1109/TC.1986.1676819.
  16. Janusz A. Brzozowski and Carl-Johan H. Seger. Asynchronous Circuits. Monographs in Computer Science. Springer, 1995. URL: https://doi.org/10.1007/978-1-4612-4210-9.
  17. Paul Caspi and Marc Pouzet. Lucid Synchrone: une extension fonctionnelle de Lustre. In Journées Francophones des Langages Applicatifs (JFLA), Morzine-Avoriaz, France, February 1999. INRIA. URL: https://hal.science/hal-01574464.
  18. Adrien Champion, Alain Mebsout, Christoph Sticksel, and Cesare Tinelli. The kind 2 model checker. In Swarat Chaudhuri and Azadeh Farzan, editors, Computer Aided Verification, pages 510-517, Cham, 2016. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-41540-6_29.
  19. Van Chan Ngo, Jean-Pierre Talpin, and Thierry Gautier. Translation validation for synchronous data-flow specification in the signal compiler. In Susanne Graf and Mahesh Viswanathan, editors, Formal Techniques for Distributed Objects, Components, and Systems, pages 66-80, Cham, 2015. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-19195-9_5.
  20. Jean-Louis Colaço, Bruno Pagano, and Marc Pouzet. SCADE 6: A formal language for embedded critical software development (invited paper). In Frédéric Mallet, Min Zhang, and Eric Madelaine, editors, 11th International Symposium on Theoretical Aspects of Software Engineering, TASE 2017, Sophia Antipolis, France, September 13-15, 2017, pages 1-11. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/TASE.2017.8285623.
  21. The Coq Development Team. The Coq Reference Manual, version 8.15.2, May 2022. Available electronically at URL: http://coq.inria.fr/doc/V8.15.2/refman/.
  22. Laurent Cosserat. Sémantique opérationnelle du langage synchrone Esterel. Thèse de docteur-ingénieur, Université de Nice, 1985. Google Scholar
  23. Philippe Couronné. Conception et implémentation du système Esterel v2. Thèse d'informatique, Université Paris VII, 1988. Google Scholar
  24. Nicolaas Govert de Bruijn. Lambda calculus notation with nameless dummies: A tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae, 34:381-392, 1972. URL: https://doi.org/10.1016/1385-7258(72)90034-0.
  25. Stephen A. Edwards. An esterel compiler for large control-dominated systems. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 21(2):169-183, 2002. URL: https://doi.org/10.1109/43.980257.
  26. Bernard Espiau and Ève Coste-Manière. A synchronous approach for control sequencing in robotics applications. In Proc. IEEE International Workshop on Intelligent Motion, Istambul, pages 503-508, 1990. Google Scholar
  27. Esterel EDA Technologies. The Esterel v7_60 reference manual. Technical report, Esterel EDA Technologies, 2008. URL: https://www.college-de-france.fr/media/gerard-berry/UPL681247605558671166_Esterelv7.60_ReferenceManual.pdf.
  28. Georges Gonthier. Sémantique et modèles d'exécution des langages réactifs synchrones; application à Esterel. Thèse d'informatique, Université d'Orsay, 1988. Google Scholar
  29. Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O'Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, and Laurent Théry. A machine-checked proof of the odd order theorem. In International Conference on Interactive Theorem Proving (ITP), pages 163-179. Lectures Notes in Computer Science 7998, Springer Verlag, 2013. URL: https://doi.org/10.1007/978-3-642-39634-2_14.
  30. Paul Le Guernic, Thierry Gautier, Michel Le Borgne, and Claude Le Maire. Programming real-time applications with SIGNAL. Proc. IEEE, 79(9):1321-1336, 1991. URL: https://doi.org/10.1109/5.97301.
  31. Nicolas Halbwachs, Paul Caspi, Pascal Raymond, and Daniel Pilaud. The synchronous data flow programming language LUSTRE. Proc. IEEE, 79(9):1305-1320, 1991. URL: https://doi.org/10.1109/5.97300.
  32. Nicolas Halbwachs, Fabienne Lagnier, and Christophe Ratel. Programming and verifying real-time systems by means of the synchronous data-flow language LUSTRE. IEEE Trans. Software Eng., 18(9):785-793, 1992. URL: https://doi.org/10.1109/32.159839.
  33. Gérard P. Huet. Confluent reductions: Abstract properties and applications to term rewriting systems: Abstract properties and applications to term rewriting systems. J. ACM, 27(4):797-821, 1980. URL: https://doi.org/10.1145/322217.322230.
  34. Delphine Kaplan-Terrasse. Vers la certification du compilateur v5 d'esterel dans coq. Technical report, Inria, 2000. in French. Google Scholar
  35. Xavier Leroy. A formally verified compiler back-end. J. Autom. Reason., 43(4):363-446, February 2009. URL: https://doi.org/10.1007/s10817-009-9155-4.
  36. Marten Lohstroh, Christian Menard, Soroush Bateni, and Edward A. Lee. Toward a lingua franca for deterministic concurrent systems. ACM Trans. Embed. Comput. Syst., 20(4):36:1-36:27, 2021. URL: https://doi.org/10.1145/3448128.
  37. Sharad Malik. Analysis of cyclic combinational circuits. In Michael R. Lightner and Jochen A. G. Jess, editors, Proceedings of the 1993 IEEE/ACM International Conference on Computer-Aided Design, 1993, Santa Clara, California, USA, November 7-11, 1993, pages 618-625. IEEE Computer Society / ACM, 1993. URL: https://doi.org/10.1109/ICCAD.1993.580150.
  38. Louis Mandel and Marc Pouzet. ReactiveML, a reactive extension to ML. In Proceedings of 7th ACM SIGPLAN International Symposium on Principles and Practice of Declarative Programming (PPDP'05), Lisbon, Portugal, 2005. URL: https://doi.org/10.1145/1069774.1069782.
  39. Florence Maraninchi. The Argos language: Graphical representation of automata and description of reactive systems. In Proc. IEEE Conf. on Visual Languages, Kobe, Japan, 1991. Google Scholar
  40. Michael Mendler, Thomas Shiple, and Gérard Berry. Constructive Boolean circuits and the exactness of timed ternary simulation. Formal Methods in System Design, 40(3):283-329, 2012. URL: https://doi.org/10.1007/s10703-012-0144-6.
  41. Gary Murakami and Ravi Sethi. Terminal call processing in Esterel. In Proc. IFIP 92 World Computer Congress, Madrid, Spain, 1992. URL: https://www.researchgate.net/publication/264871837_Terminal_Call_Processing_in_Esterel.
  42. Van Chan Ngo. Formal Verification of a Synchronous Data- flow Compiler : from Signal to C. (Vérification Formelle d'un Compilateur Synchrone: de Signal vers C). PhD thesis, University of Rennes 1, France, 2014. URL: https://tel.archives-ouvertes.fr/tel-01058041.
  43. Frank Pfenning and Christine Paulin-Mohring. Inductively defined types in the calculus of constructions. In Mathematical Foundations of Programming Semantics, pages 209-228, 1989. URL: https://doi.org/10.1007/BFb0040259.
  44. Dumitru Potop-Butucaru, Stephen A. Edwards, and Gérard Berry. Compiling Esterel. Springer, 2007. URL: https://doi.org/10.1007/978-0-387-70628-3.
  45. Claudius Ptolemaeus, editor. System Design, Modeling, and Simulation using Ptolemy II. Ptolemy.org, available as a free PDF download and low-cost paperback, 2014. URL: ptolemy.org.
  46. Valérie Roy and Robert de Simone. Auto/autograph. In Edmund M. Clarke and Robert P. Kurshan, editors, Computer Aided Verification, 2nd International Workshop, CAV '90, New Brunswick, NJ, USA, June 18-21, 1990, Proceedings, volume 531 of Lecture Notes in Computer Science, pages 65-75. Springer, 1990. URL: https://doi.org/10.1007/BFb0023720.
  47. Klaus Schneider. Proving the equivalence of microstep and macrostep semantics. In Victor Carreño, César A. Muñoz, and Sofiène Tahar, editors, Theorem Proving in Higher Order Logics, 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002, Proceedings, volume 2410 of Lecture Notes in Computer Science, pages 314-331, Berlin, Heidelberg, 2002. Springer. URL: https://doi.org/10.1007/3-540-45685-6_21.
  48. Klaus Schneider. The synchronous programming language quartz. Technical report, Internal Report 375, Department of Computer Science, University of Kaiserslautern, Kaiserslautern, Germany, 2009. URL: http://es.cs.uni-kl.de/publications/datarsg/Schn09.pdf.
  49. Ellen Sentovich, Horia Toma, and Gérard Berry. Latch optimization in circuits generated from high-level descriptions. In Proc. IEEE International Conference on Computer Aided Design, pages 428-435, 1996. URL: https://doi.org/10.1109/ICCAD.1996.569833.
  50. Manuel Serrano and Gérard Berry. Multitier programming in Hop. Communications of the ACM, 55(8):53-59, 2012. URL: https://doi.org/10.1145/2240236.2240253.
  51. Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, and Théo Winterhalter. Coq coq correct! verification of type checking and erasure for coq, in coq. Proc. ACM Program. Lang., 4(POPL):8:1-8:28, 2020. URL: https://doi.org/10.1145/3371076.
  52. Olivier Tardieu. Loops in Esterel: From Operational Semantics to Formally Specified Compilers. PhD, École Nationale Supérieure des Mines de Paris, September 2004. URL: https://pastel.archives-ouvertes.fr/pastel-00001336.
  53. Olivier Tardieu and Robert de Simone. Loops in Esterel. ACM Transactions on Embedded Computing Systems (TECS), 4(4):708-750, 2005. URL: https://doi.org/10.1145/1113830.1113832.
  54. Hervé Touati and Gérard Berry. Optimized controller synthesis using esterel. In Proc. International Workshop on Logic Synthesis IWLS'93, Lake Tahoe, 1993. URL: ftp://ftp-sop.inria.fr/meije/esterel/papers/iwls93.pdf.
  55. Reinhard von Hanxleden, Björn Duderstadt, Christian Motika, Steven Smyth, Michael Mendler, Joaquín Aguado, Stephen Mercer, and Owen O'Brien. Sccharts: sequentially constructive statecharts for safety-critical applications: Hw/sw-synthesis for a conservative extension of synchronous statecharts. In Michael F. P. O'Boyle and Keshav Pingali, editors, ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '14, Edinburgh, United Kingdom - June 09 - 11, 2014, pages 372-383, Edinburgh, UK, June 2014. ACM. URL: https://doi.org/10.1145/2594291.2594310.
  56. Reinhard von Hanxleden, Michael Mendler, Joaquín Aguado, Björn Duderstadt, Insa Fuhrmann, Christian Motika, Stephen Mercer, and Owen O'Brien. Sequentially constructive concurrency - a conservative extension of the synchronous model of computation. In Proc. Design, Automation and Test in Europe Conference (DATE'13), 2013. URL: https://doi.org/10.7873/DATE.2013.128.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact