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

Deliverable D3.1_1 v 1.0 of the Sys2soft collaborative project "Physics Aware Software"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.Une question centrale dans la conception des langages de modélisation des systèmes hybrides, y compris Modelica, est la détection, à la compilation, des circuits algébriques ou boucles de causalité. De tels circuits provoquent le blocage du modèle lors de sa simulation et empêchent la génération de code ordonnancé statiquement. Ce livrable détaille une solution à ce problème, pour un langage de modélisation hybride qui combine des equations de flots à la Lustre et des equations différentielles ordinaires. Le langage comporte un opérateur last(x) dont la valeur est la limite à gauche de la variable x. Cet opérateur permet de casser des circuits algébriques et a l'avantage de s'appliquer indifféremment sur des variables discrètes ou continues. La sémantique du langage est à base de nombres réels non-standards et définit une exécution comme une suite de pas, progressant de manière infinitésimale. Un signal est considéré causalement correct quand il peut être calculé séquentiellement et est continu en dehors des instants où un pas de calcul discret a lieu. L'analyse de causalité est définie sous la forme d'un système d'inférence de type . Il est prouvé que dans tout programme correctement typé, les signaux sont continus en dehors des seuls instants où des calculs discrets ont lieu. Cette analyse de causalité permet de générer un code de simulation ordonnancé statiquement qui fait appel à une bibliothèque standard de soldeurs de systèmes d'équations differentielles. La pertinence de cette approche est illustrée par plusieurs exemples écrits dans le langage Zélus, qui est un langage de modélisation des systèmes hybrides, qui combine des equations de flôts synchrones et des equations différentielles