The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
Synchronous languages like Lustre are ideal for programming an important class of embedded controllers. Their discrete model of time and deterministic semantics facilitate the precise expression of reactive behaviours. But, many systems are naturally modelled using physical timing constraints that inevitably involve some nondeterminism due to tolerances in requirements or uncertainties in implementations. Conversely, such constraints are readily modelled using Timed Automata and analyzed symbolically in tools like Uppaal, but large-scale discrete-time behaviours are more cumbersome to express.
Building on techniques developed for Zélus , a Lustre-like language extended with Ordinary Differential Equations, we propose a language combining dataflow equations with the invariants and guards of Timed Safety Automata. We develop a source-to-source compilation pass to generate discrete code that, coupled with standard operations on Difference-Bound Matrices, produces symbolic simulation traces.
This work is described in Chapter 6 of Guillaume Baudart's thesis  and was presented at the Forum on Specification and Design Languages in Verona last September .
Joint work with Guillaume Baudart (now at IBM Research) and Marc Pouzet (UPMC/ENS Paris/Inria).