Model checking prioritized timed automata

Shang Wei Lin, Pao Ann Hsiung, Chun Hsian Huang, Yean-Ru Chen

研究成果: Conference contribution

13 引文 斯高帕斯(Scopus)

摘要

Priorities are often used to resolve conflicts in timed systems. However, priorities are not directly supported by state-of-art model checkers. Often, a designer has to either abstract the priorities leading to a high degree of non-determinism or model the priorities using existing primitives. In this work, it is shown how prioritized timed automata can make modelling prioritized timed systems easier through the support for priority specification and model checking. The verification of prioritized timed automata requires a subtraction operation to be performed on two clock zones, represented by DBMs, for which we propose an algorithm to generate the minimal number of zones partitioned. After the application of a series of DBM subtraction operations, the number of zones generated become large. We thus propose an algorithm to reduce the final number of zones partitioned by merging some of them. A typical bus arbitration example is used to illustrate the benefits of the proposed algorithms. Due to the support for prioritization and zone reduction, we observe that there is a 50% reduction in the number of modes and 44% reduction in the number of transitions.

原文English
主出版物標題Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
頁面370-384
頁數15
DOIs
出版狀態Published - 2005 十二月 1
事件Third International Symposium on Automated Technology for Verification and Analysis, ATVA 2005 - Taipei, Taiwan
持續時間: 2005 十月 42005 十月 7

出版系列

名字Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
3707 LNCS
ISSN(列印)0302-9743
ISSN(電子)1611-3349

Other

OtherThird International Symposium on Automated Technology for Verification and Analysis, ATVA 2005
國家/地區Taiwan
城市Taipei
期間05-10-0405-10-07

All Science Journal Classification (ASJC) codes

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

指紋

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

引用此