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 is a short introduction to the language and its compiler (version 1). 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. Paper ML 2016 describes the design and implementation of SundialsML, a comprehensive OCaml interface to the Sundials library of numeric solvers for differential equations. Paper EMSOFT 2017 investigates the use of Zélus to write a standard library of control blocks, in both discrete and continuous time (e.g., integrators, filters, PIDs) relying on features available in Version 2 of the language. Paper EMSOFT 2018 describes the design principles of Zélus. Paper PLDI 2020 describes ProbZélus, a probabilistic extension of Zélus.

PLDI 2020
Guillaume Baudart, Louis Mandel, Eric Atkinson, Benjamin Sherman, Marc Pouzet, and Michael Carbin. Reactive Probabilistic Programming. In International Conference on Programming Language Design and Implementation (PLDI), London, United Kingdom, June 15-20 2020. ACM.
bib pdf

Synchronous modeling is at the heart of programming languages like Lustre, Esterel, or Scade used routinely for implementing safety critical control software, e.g., fly-by-wire and engine control in planes. However, to date these languages have had limited modern support for modeling uncertainty — probabilistic aspects of the software's environment or behavior — even though modeling uncertainty is a primary activity when designing a control system.

In this paper we present the first synchronous probabilistic programming language. ProbZelus conservatively provides the facilities of a synchronous language to write control software, with probabilistic constructs to model uncertainties and perform inference-in-the-loop.

We present the design and implementation of the language. We propose a measure-theoretic semantics of probabilistic stream functions and a simple type discipline to separate deterministic and probabilistic expressions. We demonstrate a semantics-preserving compilation into a first-order functional language that lends itself to a simple presentation of inference algorithms for streaming models. We also redesign the delayed sampling inference algorithm to provide efficient streaming inference.

Together with an evaluation on several reactive applications, our results demonstrate that ProbZelus enables the design of reactive probabilistic applications and efficient, bounded memory inference.

LNCS 10000
Albert Benveniste, Benoit Caillaud, Hilding Elmquist, Khalil Ghorbal, Martin Otter, and Marc Pouzet. Multi-mode dae models - challenges, theory and implementation. In Woeginger G. Steffen B., editor, Computing and Software Science: state of the Art and Perspectives, volume 10000 of Lecture Notes in Computer Science. Springer, 2019.

Our objective is to model and simulate Cyber-Physical Systems (CPS) such as robots, vehicles, and power plants. The structure of CPS models may change during simulation due to the desired operation, due to failure situations or due to changes in physical conditions. Corresponding models are called multi-mode. We are interested in multi-domain, component-oriented modeling as performed, for example, with the modeling language Modelica that leads naturally to Differential Algebraic Equations (DAEs). This paper is thus about multi-mode DAE systems. In particular, new methods are discussed to overcome one key problem that was only solved for specific subclasses of systems before: How to switch from one mode to another one when the number of equations may change and variables may exhibit impulsive behavior? An evaluation is performed both with the experimental modeling and simulation system Modia, a domain specific language extension of the programming language Julia, and with SunDAE, a novel structural analysis library for multi-mode DAE systems.

IEEE 2018
Albert Benveniste, Timothy Bourke, Benoît Caillaud, Jean-Louis Colaço, Cédric Pasteur, and Marc Pouzet. Building a Hybrid Systems Modeler on Synchronous Languages Principles. Proceedings of the IEEE, 2018.
bib pdf

Hybrid systems modeling languages that mix discrete and continuous time signals and systems are widely used to develop Cyber-Physical systems where control software interacts with physical devices. Compilers play a central role, statically checking source models, generating intermediate representations for testing and verification, and producing sequential code for simulation and execution on target platforms.

This paper presents a novel approach to the design and implementation of a hybrid systems language, built on synchronous language principles and their proven compilation techniques. The result is a hybrid systems modeling language in which synchronous programming constructs can be mixed with Ordinary Differential Equations (ODEs) and zero-crossing events, and a runtime that delegates their approximation to an off-the-shelf numerical solver.

We propose an ideal semantics based on non standard analysis, which defines the execution of a hybrid model as an infinite sequence of infinitesimally small time steps. It is used to specify and prove correct three essential compilation steps: (1) a type system that guarantees that a continuous-time signal is never used where a discrete-time one is expected and conversely; (2) a type system that ensures the absence of combinatorial loops; (3) the generation of statically scheduled code for efficient execution.

Our approach has been evaluated in two implementations: the academic language Zelus, which extends a language reminiscent of Lustre with ODEs and zero-crossing events, and the industrial prototype Scade Hybrid, a conservative extension of Scade 6.

ML 2018
Timothy Bourke, Jun Inoue, and Marc Pouzet. Sundials/ML: connecting OCaml to the Sundials numeric solvers. Electronic Proceedings in Theoretical Computer Science, 285:101–130, 2018. Extended version of paper appearing in the ACM Workshop on ML, 2016.
bib DOI pdf

This paper describes the design and implementation of a comprehensive OCaml interface to the Sundials library of numeric solvers for ordinary differential equations, differential algebraic equations, and non-linear equations. The interface provides a convenient and memory-safe alternative to using Sundials directly from C and facilitates application development by integrating with higher-level language features, like garbage-collected memory management, algebraic data types, and exceptions. Our benchmark results suggest that the interface overhead is acceptable: the standard examples are rarely twice as slow in OCaml than in C, and often less than 50% slower. The challenges in interfacing with Sundials are to efficiently and safely share data structures between OCaml and C, to support multiple implementations of vector operations and linear solvers through a common interface, and to manage calls and error signalling to and from OCaml. We explain how we overcame these difficulties using a combination of standard techniques such as phantom types and polymorphic variants, and carefully crafted data representations.

Timothy Bourke, Francois Carcenac, Jean-Louis Colaço, Bruno Pagano, Cédric Pasteur, and Marc Pouzet. A Synchronous Look at the Simulink Standard Library. In ACM International Conference on Embedded Software (EMSOFT), Seoul, October 15-20 2017.
bib pdf

Hybrid systems modelers like Simulink come with a rich collection of discrete-time and continuous-time blocks. Most blocks are not defined in terms of more elementary ones—and some cannot be—but are instead written in imperative code and explained informally in a reference manual. This raises the question of defining a minimal set of orthogonal programming constructs such that most blocks can be programmed directly and thereby given a specification that is mathematically precise, and whose compiled version performs comparably to handwritten code. In this paper, we show that a fairly large set of blocks from the Simulink standard library can be programmed in a precise, purely functional language using stream equations, hierarchical automata, Ordinary Differential Equations (ODEs), and deterministic synchronous parallel composition. Some blocks cannot be expressed as they mix discrete-time and continuous-time signals in unprincipled ways and so are statically forbidden by the type checker.

The experiment is conducted in Zélus, a synchronous language that conservatively extends Lustre with constructs for programming systems that mix discrete-time and continuous-time signals.

HSCC 2017
Albert Benveniste, Benoit Caillaud, Hilding Elmqvist, Khalil Ghorbal, Martin Otter, and Marc Pouzet. Structural Analysis of Multi-Mode DAE Systems. In International Conference on Hybrid Systems: Computation and Control (HSCC), Pittsburgh, USA, April 18-20 2017. ACM.
bib pdf

Differential Algebraic Equation (DAE) systems constitute the mathematical model supporting physical modeling languages such as Modelica, VHDL-AMS, or Simscape. Unlike ODEs, they exhibit subtle issues because of their implicit latent equations and related differentiation index. Multi-mode DAE (mDAE) systems are much harder to deal with, not only because of their mode-dependent dynamics, but essentially because of the events and resets occurring at mode transitions. Unfortunately, the large literature devoted to the numerical analysis of DAEs does not cover the multi-mode case. It typically says nothing about mode changes. This lack of foundations cause numerous difficulties to the existing modeling tools. Some models are well handled, others are not, with no clear boundary between the two classes. In this paper we develop a comprehensive mathematical approach to the structural analysis of mDAE systems which properly extends the usual analysis of DAE systems. We define a constructive semantics based on nonstandard analysis and show how to produce execution schemes in a systematic way.

Guillaume Baudart. A Synchronous Approach to Quasi-Periodic Systems. PhD thesis, École normale supérieure, 45 rue d'Ulm, 75230 Paris, 2017.
bib pdf

In this thesis we study embedded controllers implemented as sets of unsynchronized periodic processes. Each process activates quasi-periodically, that is, periodically with bounded jitter, and communicates with bounded transmission delays. Such reactive systems, termed quasi-periodic, exist as soon as two periodic processes are connected together. In the distributed systems literature they are also known as synchronous real- time models. We focus on techniques for the design and analysis of such systems without imposing a global clock synchronization. Synchronous languages were introduced as domain specific languages for the design of reactive systems. They offer an ideal framework to program, analyze, and verify quasi- periodic systems. Based on a synchronous approach, this thesis makes contributions to the treatment of quasi-periodic systems along three themes: verification, implementation, and simulation. Verification: The quasi-synchronous abstraction is a discrete abstraction proposed by Paul Caspi for model checking safety properties of quasi-periodic systems. We show that this abstraction is not sound in general and give necessary and sufficient conditions on both the static communication graph of the application and the real-time characteristics of the architecture to recover soundness. We then generalize these results to multirate systems. Implementation: Loosely time-triggered architectures are protocols designed to ensure the correct execution of an application running on a quasi-periodic system. We propose a unified framework that encompasses both the application and the protocol controllers. This framework allows us to simplify existing protocols, propose optimized versions, and give new correctness proofs. We instantiate our framework with a protocol based on clock synchronization to compare the performance of the two approaches. Simulation: Quasi-periodic systems are but one example of timed systems involving real-time characteristics and tolerances. For such nondeterministic models, we propose a symbolic simulation scheme inspired by model checking techniques for timed automata. We show how to compile a model mixing nondeterministic continuous-time and discrete-time dynamics into a discrete program manipulating sets of possible values. Each trace of the resulting program captures a set of possible executions of the source program.

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), page to appear, 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:

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:

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).

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).