Combining control and data abstraction in the verification of hybrid systems - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2009

Combining control and data abstraction in the verification of hybrid systems

Résumé

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.
Fichier non déposé

Dates et versions

hal-00786360 , version 1 (08-02-2013)

Identifiants

Citer

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. pp.141-150, ⟨10.1109/MEMCOD.2009.5185390⟩. ⟨hal-00786360⟩
60 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More