A Type-based Analysis of Causality Loops
in Hybrid Systems Modelers

Albert Benveniste, Timothy Bourke, Benoit Caillaud, Bruno Pagano, and Marc Pouzet

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 Di erential 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, de ning an execution as a sequence of in nitesimally small steps. A signal is deemed causally correct when it can be computed sequentially and only changes in nitesimally 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 Zelus, a Lustre-like synchronous language extended with hierarchical automata and ODEs.

pdf