The Community for Technology Leaders
Green Image
Issue No. 06 - June (2012 vol. 61)
ISSN: 0018-9340
pp: 843-856
Pao-Ann Hsiung , National Chung Cheng University, Chiayi
Shang-Wei Lin , National Chung Cheng University, Chiayi
ABSTRACT
Real-time systems modeled by timed automata are often symbolically verified using Difference Bound Matrix (DBM) and Binary Decision Diagram (BDD) operations. When designing concurrent real-time systems with two or more processes sharing a resource, priorities are often used to schedule processes and to resolve conflicting resource requests. Concurrent real-time systems can thus be modeled by timed automata with priorities. However, model checking timed automata with priorities needs the DBM subtraction operation, whose result may not be convex, i.e., DBMs are not closed under subtraction. Thus, a partition of the resulting DBM is required. In this work, we propose Prioritized Timed Automata (PTA) and resolve all the issues related to the model checking of PTA. Two algorithms are proposed including an optimal DBM subtraction algorithm that produces the minimal number of DBM partitions, and a DBM merging algorithm that reduces the DBM partitions after a series of DBM subtractions. Application examples show the advantages of the proposed method in terms of support for the efficient verification of prioritized timed systems.
INDEX TERMS
Priority, timed automata, difference bound matrix (DBM), model checking, optimal DBM subtraction.
CITATION
Pao-Ann Hsiung, Shang-Wei Lin, "Model Checking Prioritized Timed Systems", IEEE Transactions on Computers, vol. 61, no. , pp. 843-856, June 2012, doi:10.1109/TC.2011.99
104 ms
(Ver )