Model Checking Prioritized Timed Automata

13 years 5 months ago
Model Checking Prioritized Timed Automata
Abstract. 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 nondeterminism 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 prop...
Shang-Wei Lin, Pao-Ann Hsiung, Chun-Hsian Huang, Y
Added 26 Jun 2010
Updated 26 Jun 2010
Type Conference
Year 2005
Where ATVA
Authors Shang-Wei Lin, Pao-Ann Hsiung, Chun-Hsian Huang, Yean-Ru Chen
Comments (0)