Summary

We work on the problem of the safe design of real-time control systems. Application domains are typically safety-critical systems, as in transportation (avionics, railways) or energy production systems. Both formal methods and programming/compilation issues are involved in the correct construction of such systems and their implementation.

Our special research themes are:

1. Implementations of synchronous reactive programs, generated automatically by compilation:
   • distribution (in relation with the Lustre and Lucid Synchrone languages);
   • fault tolerance (in relation with the SynDEx environment).

   (Alain Girault, Gwenael Delaval)

2. High-level design and programming methods:
   • generation of correct controllers using discrete control synthesis (in relation with the Mode Automata and Polychrony/Signal languages, and with the Sigali synthesis tool);
   • compositional construction of correct systems;
   • reactive and aspect-oriented programming.

   (Alain Girault, Gregor Goessler, Bertrand Jeannet, Pascal Fradet, Gwenael Delaval)

3. Compositional verification and abstract interpretation techniques, with applications to the high-level design methods above. (Gregor Goessler, Bertrand Jeannet)