Name
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). The proposed approach exploits the semantics of a timed automaton to procure its over-approximative abstraction. Any safety property which holds on the abstraction is guaranteed to hold on the concrete model. In the case of a spurious counter-example, 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. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1109/TASE.2010.27 | TASE |
Keywords | Field | DocType |
concrete model,over-approximative abstraction,abstraction refinement,model checking,proposed approach refines,compositional abstraction,model checking tool uppaal,compositional abstraction refinement,compositional model checking,timed systems,automated approach,formal verification,timed automaton,automata,concrete,automata theory,cost accounting,semantics | Abstraction model checking,Automata theory,Programming language,Abstraction,Model checking,Computer science,Automaton,Theoretical computer science,Real-time computing,Timed automaton,Semantics,Formal verification | Conference |
Citations | PageRank | References |
2 | 0.39 | 10 |
Authors | ||
5 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Fei He | 1 | 175 | 28.32 |
| He Zhu | 2 | 44 | 11.69 |
| William N. N. Hung | 3 | 304 | 34.98 |
| Xiaoyu Song | 4 | 318 | 46.99 |
| Ming Gu | 5 | 501 | 51.05 |