Compositional abstraction refinement for timed systems

Fei He, He Zhu, William N.N. Hung, Xiaoyu Song, Ming Gu

Research output: Chapter in Book/Report/Conference proceedingConference contribution

4 Scopus citations

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.

Original languageEnglish (US)
Title of host publicationProceedings - 2010 4th International Symposium on Theoretical Aspects of Software Engineering, TASE 2010
Pages168-176
Number of pages9
DOIs
StatePublished - 2010
Externally publishedYes
Event2010 4th International Symposium on Theoretical Aspects of Software Engineering, TASE 2010 - Taipei, Taiwan, Province of China
Duration: Aug 25 2010Aug 27 2010

Publication series

NameProceedings - 2010 4th International Symposium on Theoretical Aspects of Software Engineering, TASE 2010

Conference

Conference2010 4th International Symposium on Theoretical Aspects of Software Engineering, TASE 2010
Country/TerritoryTaiwan, Province of China
CityTaipei
Period8/25/108/27/10

All Science Journal Classification (ASJC) codes

  • Computational Theory and Mathematics
  • Software

Fingerprint

Dive into the research topics of 'Compositional abstraction refinement for timed systems'. Together they form a unique fingerprint.

Cite this