Zélus

Foreword

Zélus is a synchronous language in the style of Lustre [12] and Lucid Synchrone [8] but extended to model hybrid systems that mix discrete-time and continuous-time signals. An example is a system that mix a (discrete-time) model of real-time control software that executes in closed loop with a model of its physical environment described by a Ordinary Differential Equations. More intricate interactions between discrete- and continuous-time behaviors can be expressed, like, for instance, continuous-time PID controllers or hybrid automata with several running modes, each of them being defined by an ODEs (the so-called hybrid automata). Zélus provides basic synchronous language constructs—difference and data-flow equations, hierarchical automata, and stream function definitions—in the style of Lustre [12] and Lucid Synchrone [8]. Continuous-time dymamics are expressed by ODEs with events defined as zero-crossings.

The expressiveness of the language is deliberately constrained to statically ensure determinism and the generation of loop-free sequential code that runs in bounded time and space. Moreover, code is generated identically for both embedded targets and simulation. For source programs with ODEs, the generated sequential code is paired with a numerical solver to approximate the continuous-time dynamics. Zélus’s main features are:

  • It is a data-flow language in Single Static Assignment form: every name has only a single definition in the source code at any instant. A program is a collection of functions from signals to signals. A signal is a function from time to values. A set of signals is defined as the solution of a set of mutually recursive equations.
  • The separation between discrete-time and continuous-time signals and systems is imposed at the level of function definitions:
    1. A node is a function from discrete-time signals to discrete-time signals. A discrete-time signal is a sequence of values (a stream) as in other synchronous languages. A node is executed consecutively over the elements of a sequence of inputs to give a sequence of outputs. Nodes have no other notion of time than this succession of instants. In particular, there is no a priori ‘distance’ (time elapsed) between two instants. Outputs are produced atomically with triggering inputs, that is, instantaneously in the same discrete instant. They may depend on previous inputs; such nodes are termed stateful.
    2. A hybrid node is a function from continuous-time signals to continuous-time signals. A continuous-time signal is a signal defined on a sequence of time intervals on the real line. A hybrid node is executed on this set of instants. Only hybrid nodes may contain ODEs and detect zero-crossing events.
  • All discrete-time computations must be executed on a discrete clock. This is statically enforced by the type system, following the convention:
    A clock is termed discrete if it has been so declared or if it results from the sub-sampling a discrete clock or a zero-crossing. Otherwise, it is termed continuous.

    It is possible to reset a continuous variable defined by an ODE on a discrete clock. A zero-crossing occurs when a continuous-time signal crosses zero from a negative value to a positive one during integration. Conceptually, a timer is a particular case of a zero-crossing event, even if the actual implementation is more specific.

  • The basic types like integers, floating-point numbers, booleans, and characters are lifted from the host language OCaml. Abstract types, product types, record types, and enumerated types can either be defined directly or imported from the host language. Functions may have polymorphic types as in ML. Structured values are accessed via pattern matching.
  • Data-flow equations may be composed arbitrarily with hierarchical automata as in Lucid Synchrone and SCADE 6. The compiler ensures determinacy and the absence of infinite loops. Hierarchical automata are internally rewritten into data-flow equations.
  • The compiler is written in OCaml as a series of source-to-source and traceable transformations that ultimately yield statically scheduled sequential OCamlcode. The results of intermediate steps can be displayed. Continuous components are simulated using an off-the-shelf numerical solvers (SUNDIALS CVODE [13]) and, two built-in basic solvers (based on Matlab’s ode23 and ode45 solvers [18]).

Zélus is a research prototype that exhibits a new way of defining a hybrid systems modeling language based on the principles and techniques of synchronous languages. Its expressive power for modeling physics is limited to ODEs, unlike Modelica which is based on DAEs. Research papers on the design, semantics and implementation of Zélus are available at http://zelus.di.ens.fr.

Availability

The implementation is written in, and generates programs in OCaml, which must be installed.

Zélus, version 1.2:http://zelus.di.ens.fr
Objective Caml, version 4.02.1http://www.ocaml.org

The language is experimental and evolves continuously. Please send comments or bug reports to Timothy.Bourke@inria.fr or Marc.Pouzet@ens.fr.

This software includes the OCaml run-time system, which is copyrighted INRIA, 2015.

Thanks

This software is a research prototype that takes considerable time to develop. If you find it useful, please consider citing our work [6] and sending us comments.