A Hybrid Synchronous Language with Hierarchical Automata

Static Typing and Translation to Synchronous Code

Albert Benveniste, Timothy Bourke, Benoît Caillaud, and Marc Pouzet

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 proved 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 earlier work, 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, namely 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 statically ensures that 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. 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.

Keywords : hybrid systems, hybrid systems modelers, modeling, synchronous languages, data-flow languages, code generation

pdf