Programming languages for hybrid discrete-time/continuous-time systems

Documents and media

Download support

pdf (1.61 MB)

Abstract

Synchronous languages are enjoying great success in the programming of embedded systems such as aircraft, trains or power plants (see Gérard Berry's 2013 and 2014 lectures). Time is logically seen as the sequence of instantaneous system reactions to inputs from an external environment. This discrete abstraction makes it possible to write programs in a mathematical language, to statically guarantee their determinism and to compile them into code running in bounded memory and time. The semantics and compilation of synchronous languages are today sufficiently precise and well understood to satisfy the requirements imposed by civil avionics certification authorities for the development of the most critical parts (see Bruno Pagano's seminar on SCADE 6 software in 2013).

However, developing a real embedded system also requires the ability to model these discrete behaviors (software, circuitry) in interaction with models of physical components (e.g. hydraulic, electrical, mechanical). Hence the independent development of digital simulation languages such as Simulink, LabView or Modelica, which are de facto industry standards. Because they can combine discrete and continuous time, these hybrid system modeling languages are apparently far more expressive than synchronous languages. But a closer look reveals that discrete time is not a logical, implementation-independent time, but can depend on the instants at which the numerical solver decides to return control. This lack of a watertight boundary induces behavior that is difficult to predict, and makes it tricky to define the reference semantics needed to ensure that simulations and implementations on different platforms are equivalent.

In this talk, we will show how to build a language for modeling hybrid systems on top of a synchronous kernel by adding ordinary differential equations (ODEs). This extension is conservative with respect to an existing synchronous language (e.g. SCADE), i.e. any synchronous program retains its semantics, while its compilation remains unchanged. But the discrete synchronous part can also be used to model transitions between continuous modes. We rely on non-standard analysis to give a synchronous semantics in the presence of an ideal solver by reducing to a discrete-time system. This abstraction helps us to answer key questions: what discipline should be imposed on the combination of discrete-time and continuous-time components? What does it mean for a program combining mixed discrete/continuous signals to be causal? Under what conditions is it possible to produce the statically ordered code needed for efficient embedded code and simulations? How can we ensure that the signals given to the numerical solver are continuous during integration? Our answer to these questions is embodied in a prototype language, called Zélus, which uses several dedicated type systems, generalizes the traceable compilation of synchronous languages and interacts with an efficient numerical solver.