Publications

The CDC 2010 and JCSS 2012 papers focus on the semantics of hybrid modelers. The LCTES 2011 and EMSOFT 2011 papers describe the type system and compilation rules; the former addresses a basic dataflow language while the latter shows how to introduce hybrid automata. The HSCC 2013 paper describes practical aspects of the language and its compiler. The HSCC 2014 paper outlines some challenges in the treatment of causality in hybrid modelers and presents a Lustre-like causality analysis for Zélus. The CC 2015 paper describes how to adapt an existing synchronous compiler to generate code from hybrid models, and validates the approach in the industrial Scade Suite KCG code generator of Scade 6.


CC 2015
Timothy Bourke, Jean-Louis Colaco, Bruno Pagano, Cédric Pasteur, and Marc Pouzet. A synchronous-based code generator for explicit hybrid systems languages. In 24th International Conference on Compiler Construction (CC 2015), pages 69–88, London, UK, April 2015.
bib pdf

Modeling languages for hybrid systems are cornerstones of embedded systems development in which software interacts with a physical environment. Sequential code generation from such languages is important for simulation efficiency and for producing code for embedded targets. Despite being routinely used in industrial compilers, code generation is rarely, if ever, described in full detail, much less formalized. Yet formalization is an essential step in building trustable compilers for critical embedded software development.

This paper presents a novel approach for generating code from a hybrid systems modeling language. By building on top of an existing synchronous language and compiler, it reuses almost all the existing infrastructure with only a few modifications. Starting from an existing synchronous data-flow language conservatively extended with Ordinary Differential Equations (ODEs), this paper details the sequence of source-to-source transformations that ultimately yield sequential code. A generic intermediate language is introduced to represent transition functions. The versatility of this approach is exhibited by treating two classical simulation targets: code that complies with the FMI standard and code directly linked with an off-the-shelf numerical solver (Sundials CVODE).

The presented material has been implemented in the Zélus compiler and the industrial Scade Suite KCG code generator of Scade 6.

See also: http://zelus.di.ens.fr/cc2015.

HSCC 2014
Albert Benveniste, Timothy Bourke, Benoit Caillaud, Bruno Pagano, and Marc Pouzet. A type-based analysis of causality loops in hybrid modelers. In 17th International Conference on Hybrid Systems: Computation and Control (HSCC'14), pages 71–82, Berlin, Germany, April 2014.
bib pdf

Explicit hybrid systems modelers like Simulink/Stateflow allow for programming both discrete- and continuous-time behaviors with complex interactions between them. A key issue in their compilation is the static detection of algebraic or causality loops. Such loops can cause simulations to deadlock and prevent the generation of statically scheduled code.

This paper addresses this issue for a hybrid modeling language that combines synchronous data-flow equations with Ordinary Differential Equations (ODEs). We introduce the operator last(x) for the left-limit of a signal x. This operator is used to break causality loops and permits a uniform treatment of discrete and continuous state variables. The semantics relies on non-standard analysis, defining an execution as a sequence of infinitesimally small steps. A signal is deemed causally correct when it can be computed sequentially and only changes infinitesimally outside of announced discrete events like zero-crossings. The causality analysis takes the form of a type system that expresses dependences between signals. In well-typed programs, signals are provably continuous during integration provided that imported external functions are also continuous.

The effectiveness of this system is illustrated with several examples written in Zélus, a Lustre-like synchronous language extended with hierarchical automata and ODEs.

See also: http://zelus.di.ens.fr/hscc2014.

HSCC 2013
Timothy Bourke and Marc Pouzet. Zélus: A synchronous language with ODEs. In 16th International Conference on Hybrid Systems: Computation and Control (HSCC'13), pages 113–118, Philadelphia, USA, March 2013.
bib pdf

Zélus is a new programming language for modeling systems that mix discrete logical time and continuous time behaviors. From a user's perspective, its main originality 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.

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. The resultant code is paired with an off-the-shelf numeric solver.

We show that it is possible to build a modeler for explicit hybrid systems à la Simulink/Stateflow on top of an existing synchronous language, using it both as a semantic basis and as a target for code generation.

JCSS 2012
Albert Benveniste, Timothy Bourke, Benoit Caillaud, and Marc Pouzet. Non-standard semantics of hybrid systems modelers. Journal of Computer and System Sciences, 78:877–910, May 2012.
bib DOI pdf

Hybrid system modelers have become a corner stone of complex embedded system development. Embedded systems include not only control components and software, but also physical devices. In this area, Simulink is a de facto standard design framework, and Modelica a new player. However, such tools raise several issues related to the lack of reproducibility of simulations (sensitivity to simulation parameters and to the choice of a simulation engine).

In this paper we propose using techniques from non-standard analysis to define a semantic domain for hybrid systems. Non-standard analysis is an extension of classical analysis in which infinitesimal (the ɛ and η in the celebrated generic sentence for all ɛ there exists η... of college maths) can be manipulated as first class citizens. This approach allows us to define both a denotational semantics, a constructive semantics, and a Kahn Process Network semantics for hybrid systems, thus establishing simulation engines on a sound but flexible mathematical foundation. These semantics offer a clear distinction between the concerns of the numerical analyst (solving differential equations) and those of the computer scientist (generating execution schemes).

We also discuss a number of practical and fundamental issues in hybrid system modelers that give rise to non reproducibility of results, nondeterminism, and undesirable side effects. Of particular importance are cascaded mode changes (also called “zero-crossings” in the context of hybrid systems modelers).

EMSOFT 2011
Albert Benveniste, Timothy Bourke, Benoit Caillaud, and Marc Pouzet. A hybrid synchronous language with hierarchical automata: Static typing and translation to synchronous code. In ACM SIGPLAN/SIGBED Conference on Embedded Software (EMSOFT'11), Taipei, Taiwan, October 2011.
bib DOI pdf

Hybrid modeling tools such as Simulink have evolved from simulation platforms into development platforms on which simulation, testing, formal verification and code generation are performed. It is thus critical to place them on a firm semantical basis where it can be proven that the results of simulation, compilation and verification are mutually consistent. Synchronous languages have addressed these issues but only for discrete systems. They cannot be used to model hybrid systems with both efficiency and precision.

Following the approach of Benveniste et al., we present the design of a hybrid modeler built from a synchronous language and an off-the-shelf numerical solver. The main novelty is a language which includes control structures, such as hierarchical automata, for both continuous and discrete contexts. These constructs can be arbitrarily mixed with data-flow and ordinary differential equations (ODEs). A type system is required to statically ensure that all discrete state changes are aligned with zero-crossing events and that the function passed to the numerical solver is free of side-effects during integration. We show that well-typed programs can be compiled through a source-to-source translation into synchronous code which is then translated into sequential code using an existing synchronous language compiler.

Based on the presented material, a compiler for a new synchronous language with hybrid features has been developed. We demonstrate its effectiveness on some examples.

LCTES 2011
Albert Benveniste, Timothy Bourke, Benoit Caillaud, and Marc Pouzet. Divide and recycle: types and compilation for a hybrid synchronous language. In ACM SIGPLAN/SIGBED Conference on Languages, Compilers, Tools and Theory for Embedded Systems (LCTES'11), Chicago, USA, April 2011.
bib DOI pdf

Hybrid modelers such as Simulink have become corner stones of embedded systems development. They allow both discrete controllers and their continuous environments to be expressed in a single language. Despite the availability of such tools, there remain a number of issues related to the lack of reproducibility of simulations and to the separation of the continuous part, which has to be exercised by a numerical solver, from the discrete part, which must be guaranteed not to evolve during a step.

Starting from a minimal, yet full-featured, Lustre-like synchronous language, this paper presents a conservative extension where data-flow equations can be mixed with ordinary differential equations (ODEs) with possible reset. A type system is proposed to statically distinguish discrete computations from continuous ones and to ensure that signals are used in their proper domains. We propose a semantics based on non-standard analysis which gives a synchronous interpretation to the whole language, clarifies the discrete/continuous interaction and the treatment of zero-crossings, and also allows the correctness of the type system to be established.

The extended data-flow language is realized through a source-to-source transformation into a synchronous subset, which can then be compiled using existing tools into routines that are both efficient and bounded in their use of memory. These routines are orchestrated with a single off-the-shelf numerical solver using a simple but precise algorithm which treats causally-related cascades of zero-crossings. We have validated the viability of the approach through experiments with the SUNDIALS library.

CDC 2010
Albert Benveniste, Benoit Caillaud, and Marc Pouzet. The fundamentals of hybrid systems modelers. In 49th IEEE International Conference on Decision and Control (CDC), Atlanta, Georgia, USA, December 2010.
bib DOI pdf

Hybrid systems modelers have become the corner stone of embedded system development, with Simulink a de facto standard and Modelica a new player. Such tools still raise a number of issues that, we believe, require more fundamental understanding.

In this paper we propose using non standard analysis as a semantic domain for hybrid systems — non standard analysis is an extension of classical analysis in which infinitesimals (the ɛ and η in the celebrated generic sentence for all ɛ. there exists η... in college maths) can be manipulated as first class citizens. This allows us to provide a denotational semantics and a constructive semantics for hybrid systems, thus establishing simulation engines on a firm mathematical basis. In passing, we cleanly separate the job of the numerical analyst (solving differential equations) from that of the computer scientist (generating execution schemes).