Zélus: a synchronous language with Ordinary Differential Equations, seminar by Timothy Bourke, INRIA

Abstract

Tools for modeling hybrid systems—like Modelica, LabView, and Simulink/Stateflow—are rightly understood and studied as programming languages. Indeed, models are now used not only for simulation, but also for test-case generation, formal verification, and translation to embedded code. Important underlying issues include defining rules for composing discrete and continuous elements, analyzing the causality of communications between those elements, and providing efficient, and eventually certifiable, compilation to sequential code either for direct execution on an embedded platform or for simulation by numerical approximation.

In this talk, I will show that these issues challenge even such high-quality and widely-used tools as Simulink/Stateflow, and present a language called Zélus that we are developing to understand and address them. The main originality of Zélus, from a user's perspective, is to extend an existing Lustre-like synchronous language with Ordinary Differential Equations (ODEs). The extension is conservative: any synchronous program expressed as data-flow equations and hierarchical automata can be composed arbitrarily with ODEs in the same source code. The underlying mathematical model is the synchronous parallel composition of stream equations, ODEs, and imperative features.

Zélus shows that it is possible to build a modeler for explicit hybrid systems using an existing synchronous language as both a semantic basis and a target for code generation. A dedicated type system and causality analysis ensure that all discrete changes are aligned with zero-crossing events so that no side effects or discontinuities occur during integration. Programs are statically scheduled and translated into sequential code that, by construction, runs in bounded time and space. Compilation is effected by source-to-source translation into a small synchronous subset which is processed by a standard synchronous compiler architecture.

In collaboration with:
  Albert Benveniste (Inria)
  Benoit Caillaud (Inria)
  Marc Pouzet (UPMC, ENS, and Inria)

Biography

Timothy Bourke is currently a researcher at INRIA Paris-Rocquencourt in the team [PARKAS]. His research focuses on languages for programming and analysing embedded systems and modelling their physica environments---one such example is the Zélus language. Prior to his current position, Dr Bourke worked in the verification group at NICTA in Sydney. He completed his PhD at UNSW in 2009.

Date/time: 
Wednesday, June 4, 2014,
10:00 to 12:30
Location: 
SICS Swedish, room von Neumann
Isafjordsgatan 22
Kista
Sweden
SE