papers.bib
@inproceedings{CDC2010,
author = {Albert Benveniste and Benoit Caillaud and Marc Pouzet},
title = {The Fundamentals of Hybrid Systems Modelers},
booktitle = {49th IEEE International Conference on Decision and Control (CDC)},
year = 2010,
address = {Atlanta, Georgia, USA},
month = dec,
url = {http://www.di.ens.fr/~pouzet/bib/cdc10.pdf},
doi = {10.1109/CDC.2010.5717614},
abstract = {
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 \emph{non standard analysis} as a
semantic domain for hybrid systems --- non standard analysis is an
extension of classical analysis in which infinitesimals (the
$\varepsilon$ and $\eta$ in the celebrated generic sentence
$\forall\ \varepsilon. \exists\ \eta \dots$ 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).
}
}
@inproceedings{LCTES2011,
author = {Albert Benveniste and Timothy Bourke and
Benoit Caillaud and Marc Pouzet},
title = {Divide and recycle: types and compilation for a
hybrid synchronous language},
booktitle = {ACM SIGPLAN/SIGBED Conference on Languages, Compilers,
Tools and Theory for Embedded Systems (LCTES'11)},
month = apr,
year = 2011,
address = {Chicago, USA},
url = {http://www.di.ens.fr/~pouzet/bib/lctes11.pdf},
doi = {10.1145/1967677.1967687},
abstract = {
Hybrid modelers such as Simulink have become corner stones of embedded
systems development. They allow both \emph{discrete} controllers
and their \emph{continuous} environments to be expressed \emph{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 \emph{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.
}
}
@inproceedings{EMSOFT2011,
author = {Albert Benveniste and Timothy Bourke and
Benoit Caillaud and Marc Pouzet},
title = {A Hybrid Synchronous Language with Hierarchical
Automata: Static Typing and Translation to Synchronous
Code},
booktitle = {ACM SIGPLAN/SIGBED Conference on Embedded Software (EMSOFT'11)},
month = oct,
year = 2011,
address = {Taipei, Taiwan},
url = {http://www.di.ens.fr/~pouzet/bib/emsoft11.pdf},
doi = {10.1145/2038642.2038664},
abstract = {
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.
}
}
@article{JCSS2012,
author = {Albert Benveniste and Timothy Bourke and Benoit
Caillaud and Marc Pouzet},
title = {Non-Standard Semantics of Hybrid Systems Modelers},
journal = {Journal of Computer and System Sciences},
year = 2012,
volume = 78,
month = may,
pages = {877--910},
doi = {10.1016/j.jcss.2011.08.009},
url = {http://www.di.ens.fr/~pouzet/bib/jcsspaper.pdf},
abstract = {
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 \emph{non-standard
analysis} to define a semantic domain for hybrid systems. Non-standard
analysis is an extension of classical analysis in which infinitesimal
(the $\varepsilon$ and $\eta$ in the celebrated generic sentence
$\forall\ \varepsilon\ \exists\ \eta\dots$ 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).
}
}
@inproceedings{HSCC2013,
visiblekey = {HSCC13},
author = {Timothy Bourke and Marc Pouzet},
title = {Zélus: A Synchronous Language with {ODEs}},
booktitle = {16th International Conference on Hybrid Systems:
Computation and Control (HSCC'13)},
pages = {113--118},
month = mar,
year = 2013,
address = {Philadelphia, USA},
url = {http://www.di.ens.fr/~pouzet/bib/hscc13.pdf},
abstract = {
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 \emph{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 \emph{à la Simulink/Stateflow} on top of an existing
synchronous language, using it both as a semantic basis and as a
target for code generation.
}
}
@inproceedings{HSCC2014,
visiblekey = {HSCC14},
author = {Albert Benveniste and Timothy Bourke and Benoit Caillaud
and Bruno Pagano and Marc Pouzet},
title = {A Type-Based Analysis of Causality Loops in Hybrid Modelers},
booktitle = {17th International Conference on Hybrid Systems:
Computation and Control (HSCC'14)},
pages = {71--82},
month = apr,
year = 2014,
address = {Berlin, Germany},
url = {http://zelus.di.ens.fr/hscc2014/fullpaper.pdf},
abstract = {
Explicit hybrid systems modelers like \emph{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 \emph{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 \emph{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: \url{http://zelus.di.ens.fr/hscc2014}.
}
}
@inproceedings{CC2015,
author = {Timothy Bourke
and Jean-Louis Cola{\,{c}}o
and Bruno Pagano
and C{\'{e}}dric Pasteur
and Marc Pouzet},
title = {A Synchronous-based Code Generator For Explicit Hybrid
Systems Languages},
booktitle = {24th International Conference on Compiler Construction
(CC 2015)},
year = 2015,
pages = {to appear},
address = {London, UK},
month = apr,
url = {http://zelus.di.ens.fr/cc2015/paper.pdf},
abstract = {
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: \url{http://zelus.di.ens.fr/cc2015}.
}
}
@article{ML2018,
author = {Timothy Bourke
and Jun Inoue
and Marc Pouzet},
title = {{Sundials/ML}: connecting {OCaml} to the {Sundials}
numeric solvers},
publisher = {{Open Publishing Association}},
journal = {Electronic Proceedings in Theoretical Computer Science},
volume = 285,
pages = {101--130},
year = 2018,
doi = {10.4204/EPTCS.285.4},
note = {Extended version of paper appearing in the ACM Workshop on ML, 2016},
abstract = {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.},
url = {https://www.di.ens.fr/~pouzet/bib/paper-sundialsmld2018.pdf}
}
@inproceedings{HSCC2017,
author = {Albert Benveniste and Benoit
Caillaud and Hilding Elmqvist and Khalil Ghorbal and Martin Otter and Marc Pouzet},
title = {{Structural Analysis of Multi-Mode DAE Systems}},
booktitle = {International Conference on
Hybrid Systems: Computation and Control (HSCC)},
year = 2017,
month = {April 18-20},
address = {Pittsburgh, USA},
organization = {ACM},
abstract = {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.},
url = {https://www.di.ens.fr/~pouzet/bib/hscc17.pdf}
}
@inproceedings{EMSOFT2017,
author = {Timothy Bourke and Francois Carcenac and Jean-Louis Cola\c{c}o
and Bruno Pagano and C\'edric Pasteur and Marc Pouzet},
title = {{A Synchronous Look at the Simulink Standard Library}},
booktitle = {ACM International Conference on Embedded Software (EMSOFT)},
month = {October 15-20},
address = {Seoul},
year = 2017,
abstract = {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 \emph{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\'elus, a synchronous language that
conservatively extends Lustre with constructs for
programming systems that mix discrete-time and continuous-time signals.},
url = {https://www.di.ens.fr/~pouzet/bib/emsoft17.pdf}
}
@phdthesis{PHD_BAUDART:2017,
author = {Guillaume Baudart},
title = {{A Synchronous Approach to Quasi-Periodic Systems}},
school = {\'Ecole normale sup\'erieure},
year = 2017,
address = {45 rue d'Ulm, 75230 Paris},
abstract = {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.
},
url = {https://guillaume.baudart.eu/thesis/baudart-thesis.pdf}
}
@article{IEEE2018,
author = {Albert Benveniste and Timothy Bourke
and Beno\^{\i}t Caillaud and Jean-Louis Cola\c{c}o
and C\'edric Pasteur and Marc Pouzet},
title = {{Building a Hybrid Systems Modeler on Synchronous
Languages Principles}},
journal = {Proceedings of the IEEE},
year = 2018,
abstract = { 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.},
url = {https://www.di.ens.fr/~pouzet/bib/ieee18.pdf}
}
@incollection{LNCS10000,
author = {Albert Benveniste and
Benoit Caillaud and Hilding Elmquist and Khalil Ghorbal and
Martin Otter and Marc Pouzet},
title = {Multi-Mode DAE Models - Challenges, Theory and
Implementation. },
booktitle = {Computing and Software Science: state of the Art and
Perspectives},
editor = {Steffen B., Woeginger G.},
publisher = {Springer},
year = 2019,
volume = 10000,
series = {Lecture Notes in Computer Science},
abstract = {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.}
}
@inproceedings{PLDI2020,
author = {Guillaume Baudart and Louis Mandel and
Eric Atkinson and Benjamin Sherman and Marc Pouzet and Michael Carbin},
title = {{Reactive Probabilistic Programming}},
booktitle = {International Conference on Programming Language Design and
Implementation (PLDI)},
year = 2020,
month = {June 15-20},
address = {London, United Kingdom},
organization = {ACM},
abstract = {
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 \ProbZelus the first {\em 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 {\em
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 \emph{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.},
url = {https://www.di.ens.fr/~pouzet/bib/pldi2020-extended.pdf}
}