Skip to Main content Skip to Navigation
Conference papers

Compositional Abstraction Refinement for Timed Systems

Fei He 1, 2 Lei Zhu 2 William N. N. 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.
Document type :
Conference papers
Complete list of metadata
Contributor : Bow-Yaw Wang Connect in order to contact the contributor
Submitted on : Friday, September 10, 2010 - 10:56:31 AM
Last modification on : Thursday, February 3, 2022 - 11:18:29 AM


  • HAL Id : inria-00516575, version 1



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



Record views