hal-00659698, version 1
From Hybrid Data-Flow Languages to Hybrid Automata: A Complete Translation
Peter Schrammel
a, 1Bertrand Jeannet a, 1, 2
N° RR-7859 (2012)
Résumé : Hybrid systems are used to model embedded computing systems interacting with their physical environment. There is a conceptual mismatch between high-level hybrid system languages like Simulink, which are used for simulation, and hybrid automata, the most suitable representation for safety verification. Indeed, in simulation languages the interaction between discrete and continuous execution steps is specified using the concept of zero-crossings, whereas hybrid automata exploit the notion of staying conditions. We describe a translation from a hybrid data-flow language to logico-numerical hybrid automata that treats this issue in detail. We examine various zero-crossing semantics, propose a sound translation, and discuss to which extent the original semantics is preserved.
- a – INRIA
- 1 : POP ART (INRIA Grenoble Rhône-Alpes / LIG Laboratoire d'Informatique de Grenoble)
- INRIA – Institut National Polytechnique de Grenoble (INPG) – Université Joseph Fourier - Grenoble I – Université Pierre Mendès-France - Grenoble II – CNRS : UMR5217
- 2 : Laboratoire d'Informatique de Grenoble (LIG)
- CNRS : UMR5217 – INRIA – Université Pierre Mendès-France - Grenoble II – Université Joseph Fourier - Grenoble I – Institut Polytechnique de Grenoble - Grenoble Institute of Technology
- Collaboration : INRIA Synchronics
- Domaine : Informatique/Théorie et langage formel
Informatique/Systèmes embarqués - Mots-clés : Hybrid Systems – Verification – Data-Flow Languages – Hybrid Automata – Static Analysis
- Référence interne : RR-7859
- hal-00659698, version 1
- http://hal.inria.fr/hal-00659698
- oai:hal.inria.fr:hal-00659698
- Contributeur : Peter Schrammel
- Soumis le : Samedi 28 Janvier 2012, 07:00:13
- Dernière modification le : Samedi 28 Janvier 2012, 07:00:13
Documents associés
Exporter