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

Albert Benveniste 1 Timothy Bourke 2 Benoît Caillaud 1 Bruno Pagano 3 Marc Pouzet 4, 2, 5
1 HYCOMES - Modélisation hybride & conception par contrats pour les systèmes embarqués multi-physiques
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
2 Parkas - Parallélisme de Kahn Synchrone
Inria de Paris, DI-ENS - Département d'informatique de l'École normale supérieure, CNRS - Centre National de la Recherche Scientifique
Abstract : Explicit hybrid systems modelers like 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 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 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, signals are provably continuous during integration provided that imported external functions are also continuous, and 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.
Complete list of metadatas

Cited literature [24 references]  Display  Hide  Download

https://hal.inria.fr/hal-01549183
Contributor : Benoît Caillaud <>
Submitted on : Friday, June 30, 2017 - 10:54:26 AM
Last modification on : Friday, September 13, 2019 - 9:48:42 AM
Long-term archiving on : Monday, January 22, 2018 - 9:28:57 PM

File

paper.pdf
Files produced by the author(s)

Identifiers

Citation

Albert Benveniste, Timothy Bourke, Benoît Caillaud, Bruno Pagano, Marc Pouzet. A Type-based Analysis of Causality Loops in Hybrid Systems Modelers. Nonlinear Analysis: Hybrid Systems, Elsevier, 2017, 26, pp.168-189. ⟨10.1016/j.nahs.2017.04.004⟩. ⟨hal-01549183v2⟩

Share

Metrics

Record views

2092

Files downloads

485