Synchronous Programming of Cyber-physical Systems

Abstract

Synchronous programming has enjoyed great success in the design and implementation of the most critical control software, e.g., aircraft (fly-by-wire, engine control, braking), railways (on board control, interlocking), nuclear plants (control software). Many of these applications are developed with the language SCADE, founded on pioneering work in Lustre, with key additions from Esterel and Lucid Synchrone.

Lustre is a domain specific language for programming the block diagrams that abound in engineering disciplines. It formalizes components as synchronous functions over streams (infinite sequences) expressed by recursively defined sets of dataflow equations. Models can be simulated and formally verified before being automatically compiled into code guaranteed to execute in bounded time and memory. This idea of 'model based design', radical for the time, is today at the heart of widely used industrial tools like Simulink.

This lecture will present the foundations of synchronous programming. We will come back to the origin of Lustre, its links with other stream language and the interest of a synchronous interpretation. We shall present its semantics and modular compilation to software and show how it can be specified and verified formally in an interactive theorem prover (Coq). The lecture will explain how the subtle mix of stream equations and hierarchical automata was designed and its integration into SCADE. We will see how type theory can be applied to express several safety properties and ensure a compilation into statically scheduled code for execution in finite memory, and also how those type systems can be extended for applications with multiple execution rates. Finally, I will describe the design, semantics and implementation of Zélus, where discrete controllers can be composed with continuous-time models of a physical environment.

References

- JL. Colaco, B. Pagano and M. Pouzet. Scade 6: A Formal Language for Embedded Critical Software Development. In Theoretical Aspect of Software Engineering (TASE). September 2017.

- T. Bourke, L. Brun, P.E. Dagand, X. Leroy, M. Pouzet, L.Rieg. A Formally Verified Compiler for Lustre. In Programming Language, Design and Implementation (PLDI). June 2017

- T. Bourke and M. Pouzet. Zélus, a Synchronous Language with ODEs. In Hybrid Systems: Computation and Control (HSCC). April 2013. - Zélus: see zelus.di.ens.fr for documentation and distribution.