Combining control and data abstraction in the verification of hybrid systems

Xavier Briand 1 Bertrand Jeannet 1, *
* Auteur correspondant
1 POP ART - Programming languages, Operating Systems, Parallelism, and Aspects for Real-Time
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : We address the verification of hybrid systems built as the composition of a discrete software controller interacting with a physical environment exhibiting a continuous behavior. Our goal is to attack the problem of the combinatorial explosion of discrete states that may happen if a complex software controller is considered. We propose as a solution to extend an existing abstract interpretation technique, namely dynamic partitioning, to hybrid systems described in a symbolic formalism. Dynamic partitioning allows to finely tune the tradeoff between precision and efficiency in the analysis. We show the effectiveness of the approach by a case study that combines a non trivial controller specified in the synchronous dataflow programming language Lustre with its physical environment.
Type de document :
Communication dans un congrès
Formal Methods and Models for Codesign, MEMOCODE'2009, Jul 2009, Boston, United States. IEEE, pp.141-150, 2009, 〈10.1109/MEMCOD.2009.5185390〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00786360
Contributeur : Bertrand Jeannet <>
Soumis le : vendredi 8 février 2013 - 14:16:59
Dernière modification le : mercredi 11 avril 2018 - 01:56:25

Identifiants

Collections

Citation

Xavier Briand, Bertrand Jeannet. Combining control and data abstraction in the verification of hybrid systems. Formal Methods and Models for Codesign, MEMOCODE'2009, Jul 2009, Boston, United States. IEEE, pp.141-150, 2009, 〈10.1109/MEMCOD.2009.5185390〉. 〈hal-00786360〉

Partager

Métriques

Consultations de la notice

128