This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Model Checking Prioritized Timed Systems
June 2012 (vol. 61 no. 6)
pp. 843-856
ASCII Text
x 
 
Shang-Wei Lin, Pao-Ann Hsiung, "Model Checking Prioritized Timed Systems," IEEE Transactions on Computers, vol. 61, no. 6, pp. 843-856, June, 2012.
 
 
BibTex
x
 
@article{ 10.1109/TC.2011.99,
author = {Shang-Wei Lin and Pao-Ann Hsiung},
title = {Model Checking Prioritized Timed Systems},
journal ={IEEE Transactions on Computers},
volume = {61},
number = {6},
issn = {0018-9340},
year = {2012},
pages = {843-856},
doi = {http://doi.ieeecomputersociety.org/10.1109/TC.2011.99},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - JOUR
JO - IEEE Transactions on Computers
TI - Model Checking Prioritized Timed Systems
IS - 6
SN - 0018-9340
SP843
EP856
EPD - 843-856
A1 - Shang-Wei Lin,
A1 - Pao-Ann Hsiung,
PY - 2012
KW - Priority
KW - timed automata
KW - difference bound matrix (DBM)
KW - model checking
KW - optimal DBM subtraction.
VL - 61
JA - IEEE Transactions on Computers
ER -
 
Shang-Wei Lin, National Chung Cheng University, Chiayi
Pao-Ann Hsiung, National Chung Cheng University, Chiayi
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.

[1] http://embedded.cs.ccu.edu.tw/~esl_web/Project/ Ch/SGMpta.htm, 2011.
[2] K. Altisen, G. Gössler, and J. Sifakis, “A Methodology for the Construction of Scheduled Systems,” Proc. Sixth Int'l Symp. Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT '00), pp. 106-120, Sept. 2000.
[3] K. Altisen, G. Gössler, and J. Sifakis, “Scheduler Modeling Based on the Controller Synthesis Paradigm,” Real-Time Systems, vol. 23, pp. 55-84, July 2002.
[4] R. Alur, C. Courcoubetis, and D.L. Dill, “Model-Checking for Real-Time Systems,” Proc. IEEE Fifth Ann. Symp. e Logic in Computer Science (LICS '90), pp. 414-425, June 1990.
[5] R. Alur and D.L. Dill, “A Theory of Timed Automata,” Theoretical Computer Science, vol. 126, no. 2, pp. 183-235, Apr. 1994.
[6] J.C.M. Baeten, J.A. Bergstra, and J.W. Klop, “Syntax and Defining Equations for an Interrupt Mechanism in Process Algebra,” Technical Report CS-R8503, Centre for Math. and Computer Science, 1985.
[7] J. Bengtsson, K. Larsen, F. Larsson, P. Pettersson, and Y. Wang, “UPPAAL: A Tool Suite for Automatic Verification of Real-Time Systems,” Proc. Workshop Verification and Control of Hybrid Systems III, pp. 232-243, Oct. 1995.
[8] E. Bini and G.C. Buttazzo, “Schedulability Analysis of Periodic Fixed Priority Systems,” IEEE Trans. Computers, vol. 53, no. 11, pp. 1462-1473, Nov. 2004.
[9] V. Braberman, “Modeling and Checking Real-Time System Designs,” PhD thesis, Dept. of Computation, Universidad de Bue nos Aires, 2000.
[10] G. Bruns, “A Case Study in Safety-Critical Design,” Proc. Fourth Int'l Workshop Computer-Aided Verification (CAV), pp. 220-233, June 1992.
[11] R.E. Bryant, “Graph-Based Algorithms for Boolean Function Manipulation,” IEEE Trans. Computers, vol. C-35, no. 8, pp. 677-691, Aug. 1986.
[12] J. Camilleri, “Introducing a Priority Operator to CCS,” Technical Report 157, Univ. of Cambridge, 1989.
[13] E.M. Clarke and E.A. Emerson, “Design and Sythesis of Synchronization Skeletons Using Branching Time Temporal Logic,” Proc. Logics of Programs Workshop, pp. 52-71, May 1981.
[14] E.M. Clarke, O. Grumberg, and D.A. Peled, Model Checking. MIT Press, 1999.
[15] R. Cleaveland and M. Hennessy, “Priorities in Process Algebra,” Proc. Third Symp. Logic in Computer Science, July 1988.
[16] R. Cleaveland, G. Lüttgen, V. Natarajan, and S. Sims, “Modeling and Verifying Distributed Systems Using Priorities: A Case Study,” Software—Concepts and Tools, vol. 17, no. 2, pp. 50-62, Mar. 1996.
[17] A. Cribbens, “Solid-State Interlocking (SSI): An Integrated Electronic Signalling System for Mainline Railways,” Proc. IEE Electric Power Applications, vol. 134, May 1987.
[18] A. David, “Merging DBMs Efficiently,” Proc. 17th Nordic Workshop Programming Theory, pp. 54-56, Oct. 2005.
[19] A. David, J. Håkansson, K.G. Larsen, and P. Pettersson, “Minimal DBM Substraction,” Proc. 16th Nordic Workshop Programming Theory, pp. 17-20, Oct. 2004.
[20] A. David, J. Håkansson, K.G. Larsen, and P. Pettersson, “Model Checking Timed Automata with Priorities Using DBM Subtraction,” Proc. Fourth Int'l Conf. Formal Modelling and Analysis of Timed Systems (FORMATS '06), pp. 128-142, Sept. 2006.
[21] D.L. Dill, “Timing Assumptions and Verification of Finite-state Concurrent Systems,” Proc. Workshop Automatic Verification Methods for Finite State Systems, pp. 197-212, June 1989.
[22] W.M. Elseaidy, R. Cleaveland, and J. BaughJr., “Modeling and Verifying Active Structural Control Systems,” Science of Computer Programming, vol. 29, nos. 1/2, pp. 99-122, July 1977.
[23] E. Fersman, L. Mokrushin, P. Pettersson, and Y. Wang, “Schedulability Analysis of Fixed-Priority Systems Using Timed Automata,” Theoretical Computer Science, vol. 354, no. 2, pp. 301-317, Mar. 2006.
[24] G. Gössler and J. Sifakis, “Priority Systems,” Proc. Second Int'l Symp. Formal Methods for Components and Objects (FMCO), pp. 314-329, Nov. 2003.
[25] P.-A. Hsiung and S.-W. Lin, “Model Checking Timed Systems with Priorities,” Proc. IEEE 11th Int'l Conf. Embedded and Real-Time Computing Systems and Applications (RTCSA), pp. 539-544, Aug. 2005.
[26] P.-A. Hsiung and F. Wang, “A State-Graph Manipulator Tool for Real-Time System Specification and Verification,” Proc. Fifth Int'l Conf. Real-Time Computing Systems and Applications (RTCSA), Oct. 1998.
[27] K.G. Larsen, F. Larsson, P. Pettersson, and W. Yi, “Efficient Verification of Real-Time Systems: Compact Data Structure and State-Space Reduction,” Proc. IEEE 18th Real-Time Systems Symp., pp. 14-24, Dec. 1997.
[28] J.P. Lehoczky, L. Sha, and Y. Ding, “The Rate Monotonic Scheduling Algorithm: Exact Characterization and Average Case Behavior,” Proc. IEEE Real-Time Systems Symp., pp. 166-171, Dec. 1989.
[29] S.-W. Lin, P.-A. Hsiung, C.-H. Huang, and Y.-R. Chen, “Model Checking Prioritized Timed Automata,” Proc. Third Int'l Symp. Automated Technology for Verification and Analysis (ATVA '05), pp. 370-384, Oct. 2005.
[30] C.L. Liu and J.W. Layland, “Scheduling Algorithms for Multiprogramming in a Hard-Real-Time Environment,” J. ACM, vol. 20, no. 1, pp. 46-61, 1973.
[31] G. Lowe, “Probabilities and Priorities in Timed CSP,” PhD thesis, St. Hugh's College, Univ. of Oxford, 1993.
[32] R. Milner, Communication and Concurrency. Prentice Hall, 1989.
[33] J.-P. Queille and J. Sifakis, “Specification and Verification of Concurrent Systems in CESAR,” Proc. Fifth Colloquium Int'l Symp. Programming, pp. 337-351, Apr. 1982.
[34] J. Sifakis, “The Compositional Specification of Timed Systems,” Proc. 11th Int'l Conf. Computer-Aided Verification (CAV '99), pp. 2-7, July 1999.
[35] J. Sifakis, “Modeling Real-Time Systems—Challenges and Work Directions,” Proc. First Int'l Workshop Embedded Software (EMSOFT), pp. 373-389, Oct. 2001.
[36] F. Wang, “RED: Model-Checker for Timed Automata with Clock-Restriction Diagram,” Proc. Workshop Real-Time Tools, Aug. 2001.
[37] F. Wang and P.-A. Hsiung, “Efficient and User-Friendly Verification,” IEEE Trans. Computers, vol. 51, no. 1, pp. 61-83, Jan. 2002.
[38] S. Yovine, “Kronos: A Verification Tool for Real-Time Systems,” Int'l J. Software Tools for Technology Transfer, vol. 1, nos. 1/2, pp. 123-133, Oct. 1997.

Index Terms:
Priority, timed automata, difference bound matrix (DBM), model checking, optimal DBM subtraction.
Citation:
Shang-Wei Lin, Pao-Ann Hsiung, "Model Checking Prioritized Timed Systems," IEEE Transactions on Computers, vol. 61, no. 6, pp. 843-856, June 2012, doi:10.1109/TC.2011.99
Usage of this product signifies your acceptance of the Terms of Use.