LSV Seminar

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.

Past Seminars

Compiling a Synchronous Language with Timers for Simulation

Timothy Bourke
Date
Tuesday, January 30 2018 at 11:00AM
Place
Salle Condorcet (Bât. d'Alembert)
Speaker
Timothy Bourke (ENS Paris)

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 [1], 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 [2] and was presented at the Forum on Specification and Design Languages in Verona last September [3]. Joint work with Guillaume Baudart (now at IBM Research) and Marc Pouzet (UPMC/ENS Paris/Inria).

[1]: http://zelus.di.ens.fr
[2]: https://hal.inria.fr/tel-01507595
[3]: https://hal.inria.fr/hal-01575621

About LSV