Esterel Technologies

Scientific Historic Background

Synchronous models and languages appeared independently in the beginning of the 1980's. Esterel was defined by Gerard Berry in Sophia-Antipolis ¹². Lustre was defined by P. Caspi and N. Halbwachs in Grenoble³. Signal was developed by A. Benveniste and P. Le Guernic in Rennes⁴ In Israel, D. Harel introduced the Statecharts quasi-synchronous graphical formalism⁵. In Grenoble, F. Maraninchi defined the Argos formalism⁶ that makes (restricted) Statecharts drawings fully synchronous. More recently, in Nice, C. Andre extended Argos into the SyncCharts formalism⁷ that has the same expressive power as Esterel. Synchronous programming was also introduced in the framework of concurrent constraint programming by V. Saraswat et. al.⁸⁹. See¹⁰ for a joint presentation of Argos, Esterel, Lustre, and Signal.

R. Milner also introduced a form of synchrony primitive in his SCCS process calculus¹¹; D. Austry and G. Boudol developed Milner's synchronous approach further in the Meije calculus¹². The SCCS and Meije calculi are somewhat weaker than the aforementioned languages since they do not support negation, i.e. instantaneous test for signal absence. Nevertheless, they are useful to us for verification purposes.

The synchronous model and languages caught on quite easily in the automatic control community, where they did not fundamentally depart from models implicitly already in use in these areas. Esterel, Lustre, and Signal were actually designed and developed in mixed Control Theory and Computer Science teams¹³. The languages also entered the field of hardware design in the beginning of the 90's¹⁴¹⁵, when it was realized that the synchronous model was identical to the zero-delay model of circuits¹⁶. Being somewhat unclassical compared to prevalent CSP or CCS based models, it took more time for the synchronous model to be accepted in the mainstream Computer Science community.

From the very beginning, the authors of synchronous languages developed or helped to develop software systems to support them and submitted them to industrial experimentation. The interest for synchronous languages in industry has grown steadily, and today, industrial uses of these languages are deployed worldwide.

The development of synchronous languages has borrowed techniques from a number of usually disconnected fields. We already mentioned Control Theory. The semantics are given using Scott's midpoint semantics and Plotkin's Structural Operational Semantics techniques¹⁷. The compilers are developed directly from the semantics, following the example of Robin Milner's ML language¹⁸, itself in the line of Landin's viewpoint¹⁹. Automata theory techniques are used in the compilers²⁰²¹. Process calculi techniques such as bisimulation²²² or testing²³²⁴ play a major role in program verification, as well as abstract interpretation techniques²⁵. Synchronous hardware design, optimization, and verification techniques based on logic simplification techniques or on Binary Decision Diagrams²⁶²⁷²⁸ are now of prominent use in implementation and verification. Finally, constructive logic techniques as well as asynchronous hardware analysis techniques²⁹ turned out to be fundamental for solving the particularly important semantical causality problem for Esterel ³⁰.

Notes

1 G. Berry, S. Moisan, and J-P. Rigault. Esterel: Towards a synchronous and semantically sound high-level language for real-time applications. In Proc. IEEE Real- Time Systems Symposium, Arlington, JVirginia, IEEE Catalog 83CH1941-4, pages 30-40, 1983.

2 G. Berry and G. Gonthier. The Esterel synchronous programming language: Design, semantics implementation. Science Of Computer programming, 19(2):87-152, 1992.

3 N. Halbwachs, P. Caspi and D. Pilaud. The synchronous dataflow programming language Lustre. Another Look at Real Time Programming, Proceedings of the IEEE, Special Issue, Sept. 1991.

4 P. Le Guernic, M. Le Borgne, T. Gauthier, and C. Le Maire. Programming real time applications with Signal. Another Look at Real Time Programming, Proceedings of the IEEE Special Issue, Sept. 1991.

5 D. Harel. Statecharts: a visual approach to complex systems. Science of Computer Programming, 8:231-274 1987.

6 F. Maraninchi. The Argos language: graphical representation of automata and description of reactive systems. In International Conference on Visual Languages, Kobe, Japan, 1991.

7 C. André. Representation and analysis of reactive behaviors: A synchronous approach. In Proc. CRSA 96 Lille France July 1996.

8 V. A. Saraswat, R. Jagadeesan, and V. Gupta. Foundations of timed concurrent constrained programming. In S. Abramsky, editor, Proc. 9th Ann. IEEE Symp. on Logic in Computer Science. IEEE Computer Press 1994.

9 V. A. Saraswat, R. Jagadeesan, and V. Gupta. Default timed concurrent constraint programming. In Proc. POPL'95 San Francisco USA, pages 272-285, 1995.

10 N. Halbwachs. Synchronous Programming of Reactive Systems. Kluwer, 1993.

11 R. Milner. Calculi for synchrony and asynchrony. Theoretical Computer Science, 25:267-310: 1983.

12 D. Austry and G. Boudol. Algèbre de processus et synchronisations. Theoretical Computer Science, 30(1):91-131, 1984.

13 The control-theory designers were Jean-paul Rigault and Jean-paul Marmorat for Esterel, Paul Caspi for Lustre and Albert Benveniste for Signal.

14 G. Berry. Esterel on hardware. Philosophical Transactions Royal Society of London A, 339:87-104: 1992.

15 H. Touati and G. Berry. Optimized controller synthesis using Esterel. In Proc. International Workshop on Logic Synthesis IWLS'93, Lake Tahoe, 1993.

16 Thanks to Jean Vuillemin and Patrice Bertin at Digital Equipment Paris Research Laboratory; with them Gerard Berry also developed the 2z synchronous language based on 2-adic number theory³¹, not presented here.

17 G. Plotkin. A structural approach to operational semantics. Technical Report report DAIMI FN-19 University of Aarhus 1981.

18 R. Milner, M. Tofte, and R. Harper. The definition of Standard ML. MIT Press, 1991.

19 P.J. Landin. The next 700 programming languages. Comm. ACM, 9:157166, 1966.

20 J. Brzozowski. Derivatives of regular expressions. Journal of the ACM, 11(4), 1964.

21 G. Berry and R. Sethi. From regular expressions to deterministic automata. Theoretical Computer Science, 48:117-126 1986.

22 R. Milner. Communication and Concurrency. Prentice-Hall International, Englewood Cliffs, 1989.

23 M. Hennessy. Algebraic Theory of Processes. MIT Press, Cambridge, Massachusetts 1988.

24 N. Halbwachs, F. Lagnier and P. Raymond. Synchronous observers and the verification of reactive systems. In Proc. AMAST'93 june 1993.

25 N. Halbwachs. Delay analysis in synchronous programs. In Proc. CAV'93 pages 333-346, 1993.

26 0. Coudert, C. Berthet, and J. C. Madre. Verification of Sequential Machines Based on Symbolic execution. In Proceedings of the Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, France, 1989.

27 R.K. Brayton, G.D. Hachtel, and A.L. Sangiovanni-Vincentelli. Multilevel Logic Synthesis. Proceedings of the IEEE, 78(2):264-300, February 1990.

28 R.E. Bryant. Symbolic Boolean Manipulation with Ordered BinaryDecision Diagrams. ACM Computing Surveys, 24(3):293-318, September 1992.

29 J. Brzozowski and C.-J. Seger. Asynchronous Circuits. Springer-Verlag, 1996.

30 T. Shiple, G. Berry, and H. Touati. Constructive analysis of cyclic circuits. In Proc. International Design and Test Conference ITDC 96, Paris, France, 1996.

31J. Vuillemin. On circuits and numbers. IEEE Transactions on Computers, 43:8:868:27-79, 1994.