Model checking timed systems with urgencies

Pao Ann Hsiung, Shang Wei Lin, Yean Ru Chen, Chun Hsian Huang, Jia Jen Yeh, Hong Yu Sun, Chao Sheng Lin, Hsiao Win Liao

研究成果: Conference contribution

3 引文 斯高帕斯(Scopus)


Computation tree logic (CTL) model checkers either allow modeling of only lazy semantics in the timed system model or consider at most a simple as soon as possible semantics. However, the design of real-time systems requires different types of urgencies, which have been modeled by several urgency variants of the timed automata model. Except for the IF toolset that model checks timed automata with urgency against observers, the urgency variants of timed automata have not yet been used for verifying the satisfaction of CTL properties in real-time systems. This work is targeted at proposing a zone-based urgency semantics that is time-reactive and at model checking timed automata models that have been extended with such urgency semantics for delayable and eager transition types. Interactions among these different types of transition urgencies are also investigated. The proposed verification methods were implemented in the SGM CTL model checker and applied to real-time and embedded systems. Several experiments, comparing the state space sizes produced by SGM with that by the IF toolset, show that SGM produces much smaller state-spaces.

主出版物標題Automated Technology for Verification and Analysis - 4th International Symposium, ATVA 2006, Proceedings
發行者Springer Verlag
ISBN(列印)3540472371, 9783540472377
出版狀態Published - 2006
事件4th International Symposium on Automated Technology for Verification and Analysis, ATVA 2006 - Beijing, China
持續時間: 2006 10月 232006 10月 26


名字Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
4218 LNCS


Other4th International Symposium on Automated Technology for Verification and Analysis, ATVA 2006

All Science Journal Classification (ASJC) codes

  • 理論電腦科學
  • 電腦科學(全部)


深入研究「Model checking timed systems with urgencies」主題。共同形成了獨特的指紋。