A Type-Based Analysis of Causality Loops in Hybrid Modelers

Albert Benveniste 1 Benoît Caillaud 1 Bruno Pagano 2 Marc Pouzet 3, 4, 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
5 Parkas - Parallélisme de Kahn Synchrone
DI-ENS - Département d'informatique de l'École normale supérieure, ENS Paris - École normale supérieure - Paris, 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 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 changes infinitesimally 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 Zélus, a Lustre-like synchronous language extended with hierarchical automata and ODEs.
Type de document :
Communication dans un congrès
HSCC '14: International Conference on Hybrid Systems: Computation and Control, Apr 2014, Berlin, Germany. ACM Press, Proceedings of the 17th international conference on Hybrid systems: computation and control (HSCC 2014), pp.13, 2014, Proceedings of the 17th international conference on Hybrid systems: computation and control (HSCC '14). 〈http://2014.hscc-conference.org/〉. 〈10.1145/2562059.2562125〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01093388
Contributeur : Timothy Bourke <>
Soumis le : mercredi 10 décembre 2014 - 15:46:15
Dernière modification le : mercredi 2 août 2017 - 10:06:52

Identifiants

Citation

Albert Benveniste, Benoît Caillaud, Bruno Pagano, Marc Pouzet. A Type-Based Analysis of Causality Loops in Hybrid Modelers. HSCC '14: International Conference on Hybrid Systems: Computation and Control, Apr 2014, Berlin, Germany. ACM Press, Proceedings of the 17th international conference on Hybrid systems: computation and control (HSCC 2014), pp.13, 2014, Proceedings of the 17th international conference on Hybrid systems: computation and control (HSCC '14). 〈http://2014.hscc-conference.org/〉. 〈10.1145/2562059.2562125〉. 〈hal-01093388〉

Partager

Métriques

Consultations de la notice

883