Compositional Abstraction Refinement for Timed Systems

Fei He 1, 2 Lei Zhu 2 William Hung 3 Xiaoyu Song 1 Ming Gu 1, 2
1 FORMES - Formal Methods for Embedded Systems
LIAMA - Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées, Inria Paris-Rocquencourt
Abstract : Model checking suffers from the state explosion problem. Compositional abstraction and abstraction refinement have been investigated in many areas to address this problem. This paper considers the compositional model checking for timed systems. We present an automated approach which combines compositional abstraction and counter-example guided abstraction refinement (CEGAR). Given a timed system, the proposed approach exploits the semantics of timed automata to procure its abstraction. Our approach is conservative. Hence, any safety property which holds on the abstraction is guaranteed to hold on the concrete model. In the case of a spurious counterexample, our proposed approach refines and strengthens the abstraction in a component-wise method. We implemented our method with the model checking tool Uppaal. Experimental results show promising improvements.
Type de document :
Communication dans un congrès
IEEE International Symposium on Theoretical Aspects of Software Engineering, Aug 2010, Taipei, Taiwan. 2010
Liste complète des métadonnées

https://hal.inria.fr/inria-00516575
Contributeur : Bow-Yaw Wang <>
Soumis le : vendredi 10 septembre 2010 - 10:56:31
Dernière modification le : mercredi 10 octobre 2018 - 14:28:10

Identifiants

  • HAL Id : inria-00516575, version 1

Collections

Citation

Fei He, Lei Zhu, William Hung, Xiaoyu Song, Ming Gu. Compositional Abstraction Refinement for Timed Systems. IEEE International Symposium on Theoretical Aspects of Software Engineering, Aug 2010, Taipei, Taiwan. 2010. 〈inria-00516575〉

Partager

Métriques

Consultations de la notice

324