LSV Seminar

Date

25.02.2020, 11:00

Place

Pavillon des Jardins

Speaker

Marc Pouzet (Universite Pierre et Marie Curie, Ecole normale superieure)

The synchronous methodology has been invented in the 80's for designing and implementing real time control software, allowing to write a mathematically precise specification from which simulation, test, formal verification and the generation of embedded code are performed. It has been realized in various programming languages. For example, the synchronous language Scade 6 is now routinely used to develop safety critical software in planes or trains. Synchronous language are limited to discrete-time systems only. They do not not model, nor faithfully nor efficiently hybrid systems that mix discrete and continuous-time behaviors. This creates a gap in the development chain, with one language for hybrid systems modeling and an other for the implementation. In this talk, I will present the current development of Zelus. From a user's perspective, its originality is to extend an existing synchronous language like Lustre with Ordinary Differential Equations (ODEs) and zero-crossing events. The extension is conservative: it can be used as a normal synchronous language, that is with no change in the semantics nor compilation. But it also allow to write in the very same source both a discrete-time model and a continuous-time one, for example to model a physical device. A dedicated type system and causality analysis rejects programs for which it cannot ensure that all discrete changes are aligned with zero-crossing events. Well-typed programs are then statically scheduled and translated into sequential code and the final code is paired with an off-the-shelf numerical solver (Sundials CVODE). I will show recent experiments, in particular the extension with higher-order functions and the impact it had on the different type-based static checking and the generation of statically scheduled code.