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},
  pages = {61--70},
  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},
  pages = {137--147},
  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 = {69--88},
  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{NAHS2017,
  author = {Albert Benveniste
		 and Timothy Bourke
		 and Beno{\^{i}}t Caillaud
		 and Bruno Pagano
		 and Marc Pouzet},
  title = {A type-based analysis of causality loops in hybrid systems
		 modelers},
  journal = {Nonlinear Analysis: Hybrid Systems},
  year = 2017,
  month = nov,
  pages = {168--189},
  volume = 26,
  url = {https://hal.inria.fr/hal-01549183/document},
  abstract = {
    Explicit hybrid systems modelers like \emph{Simulink/Stateflow} allow
    for programming both discrete- and continuous-time behaviors with
    complex interactions between them.  An important step 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$. The $\Last{x}$ operator is used to break
    causality loops and permits a uniform treatment of discrete and
    continuous state variables. The semantics of the language 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 dependencies
    between signals. In well-typed programs, (\emph{i}) signals are
    \emph{provably continuous during integration} provided that imported
    external functions are also continuous, and (\emph{ii}) \emph{sequential
    code can be generated}.

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

    See also: \url{http://zelus.di.ens.fr/nahs2016}.
  }
}
@inproceedings{EMSOFT2017,
  author = {Timothy Bourke
		 and Francois Carcenac
		 and Jean-Louis Cola{\c{c}}o
		 and Bruno Pagano
		 and C{\'{e}}dric Pasteur
		 and Marc Pouzet},
  title = {A Synchronous Look at the Simulink Standard Library},
  pages = {Article 176},
  url = {http://www.di.ens.fr/~pouzet/bib/emsoft17.pdf},
  doi = {10.1145/3126516},
  booktitle = {ACM SIGBED Conference on Embedded Software (EMSOFT'17)},
  year = 2017,
  address = {Seoul, South Korea},
  month = oct,
  publisher = {ACM Press},
  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
      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 of a standard
      library like the one provided by Simulink 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 in our setting as they mix discrete-time and continuous-time
      signals in unprincipled ways that are statically forbidden by the type
      checker.

      The experiment is conducted in Zélus, a synchronous language that
      conservatively extends Lustre with ODEs to program systems that
      mix discrete-time and continuous-time signals.
  }
}