inria-00516575, version 1
Compositional Abstraction Refinement for Timed Systems
IEEE International Symposium on Theoretical Aspects of Software Engineering (2010)
Résumé : 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.
- a – Tsinghua University
- b – Synopsys Inc.
- c – ECE Dept, Portland State University
- 1 :
- INRIA – Tsinghua University / Beijing – LIAMA
- 2 :
- Tsinghua University
- Domaine : Informatique/Logique en informatique
- inria-00516575, version 1
- http://hal.inria.fr/inria-00516575
- oai:hal.inria.fr:inria-00516575
- Contributeur :
- Soumis le : Vendredi 10 Septembre 2010, 10:56:31
- Dernière modification le : Vendredi 10 Septembre 2010, 10:56:31




Exporter