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, 5
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, ENS Paris - École normale supérieure - Paris, Inria Paris-Rocquencourt, CNRS - Centre National de la Recherche Scientifique : UMR 8548
Résumé : 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.
Type de document :
Autre publication
Deliverable D3.1_1 v 1.0 of the Sys2soft collaborative project "Physics Aware Software". 2013
Liste complète des métadonnées

Littérature citée [23 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00938866
Contributeur : Benoît Caillaud <>
Soumis le : mercredi 29 janvier 2014 - 16:33:09
Dernière modification le : mercredi 2 août 2017 - 10:08:59
Document(s) archivé(s) le : lundi 5 mai 2014 - 11:06:18

Fichier

Sys2soft_WP3.1_D3.1_1_Causalit...
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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. Deliverable D3.1_1 v 1.0 of the Sys2soft collaborative project "Physics Aware Software". 2013. 〈hal-00938866〉

Partager

Métriques

Consultations de la notice

1124

Téléchargements de fichiers

183