Software reactive systems, the design of the Esterel v5 synchronous language

In 1990, in collaboration with J. Vuillemin's team at Digital Equipment, we realized that our assumption of software synchronism matched that implicitly made by circuit designers. This enabled us to solve two crucial problems for Esterel: understanding synchronous causality and the exponential explosion in code size generated in the deterministic finite automata implementation. It also led to a better understanding of the correspondence between deterministic and non-deterministic finite automata [1]. Finally, translating programs into circuits enabled automatic formal verification of safety properties: the elevator cannot travel with the door open, the airplane cannot retract its landing gear when on the ground, and so on. The Esterel compiler was coupled with the formal verifier TiGeR by Madre, Coudert and Touati, developed in the same lab, which took advantage of new developments in the representation of Boolean functions by BDDs(Binary Decision Diagrams). These verifications will be the subject of several lectures in 2014-2015.

Esterel v5design and semantics

This lecture presented the foundations of Esterel: the synchronous hypothesis, primitive or derived temporal instructions, the induced programming style [2], the potentially exponential reduction in source size compared with classical automata methods, and the constructive semantics of the language [3] based on a constructive logic of term rewriting. The idea for this semantics comes directly from the use of constructive Boolean logic for cyclic circuits.