A Type-Based Analysis of Causality Loops In Hybrid Systems Modelers

Albert Benveniste 1 Timothy Bourke 2, 3 Benoît Caillaud 1 Bruno Pagano 4 Marc Pouzet 2, 3
1 HYCOMES - Modélisation hybride & conception par contrats pour les systèmes embarqués multi-physiques
IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL, Inria Rennes – Bretagne Atlantique
2 Parkas - Parallélisme de Kahn Synchrone
DI-ENS - Département d'informatique de l'École normale supérieure, Inria Paris-Rocquencourt, CNRS - Centre National de la Recherche Scientifique : UMR 8548
Abstract : 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 Lustre-like 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 causally correct when it can be computed sequentially and only progresses by infinitesimal steps outside of discrete events. The causality analysis takes the form of a simple type system. In well-typed programs, signals are proved continuous during integration and can be translated into sequential code for integration with off-the-shelf ODE solvers. 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.
Document type :
Other publications
Complete list of metadatas

Cited literature [23 references]  Display  Hide  Download

https://hal.inria.fr/hal-00938866
Contributor : Benoît Caillaud <>
Submitted on : Wednesday, January 29, 2014 - 4:33:09 PM
Last modification on : Thursday, February 7, 2019 - 2:42:34 PM
Long-term archiving on : Monday, May 5, 2014 - 11:06:18 AM

File

Sys2soft_WP3.1_D3.1_1_Causalit...
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00938866, version 1

Citation

Albert Benveniste, Timothy Bourke, Benoît Caillaud, Bruno Pagano, Marc Pouzet. A Type-Based Analysis of Causality Loops In Hybrid Systems Modelers. 2013. ⟨hal-00938866⟩

Share

Metrics

Record views

2508

Files downloads

310