Compositional Abstraction Refinement for Timed Systems
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.