
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
ShangWei Lin, PaoAnn Hsiung, "Model Checking Prioritized Timed Systems," IEEE Transactions on Computers, vol. 61, no. 6, pp. 843856, June, 2012.  
BibTex  x  
@article{ 10.1109/TC.2011.99, author = {ShangWei Lin and PaoAnn Hsiung}, title = {Model Checking Prioritized Timed Systems}, journal ={IEEE Transactions on Computers}, volume = {61}, number = {6}, issn = {00189340}, year = {2012}, pages = {843856}, 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  00189340 SP843 EP856 EPD  843856 A1  ShangWei Lin, A1  PaoAnn 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   
[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 RealTime and FaultTolerant Systems (FTRTFT '00), pp. 106120, Sept. 2000.
[3] K. Altisen, G. Gössler, and J. Sifakis, “Scheduler Modeling Based on the Controller Synthesis Paradigm,” RealTime Systems, vol. 23, pp. 5584, July 2002.
[4] R. Alur, C. Courcoubetis, and D.L. Dill, “ModelChecking for RealTime Systems,” Proc. IEEE Fifth Ann. Symp. e Logic in Computer Science (LICS '90), pp. 414425, June 1990.
[5] R. Alur and D.L. Dill, “A Theory of Timed Automata,” Theoretical Computer Science, vol. 126, no. 2, pp. 183235, 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 CSR8503, 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 RealTime Systems,” Proc. Workshop Verification and Control of Hybrid Systems III, pp. 232243, Oct. 1995.
[8] E. Bini and G.C. Buttazzo, “Schedulability Analysis of Periodic Fixed Priority Systems,” IEEE Trans. Computers, vol. 53, no. 11, pp. 14621473, Nov. 2004.
[9] V. Braberman, “Modeling and Checking RealTime System Designs,” PhD thesis, Dept. of Computation, Universidad de Bue nos Aires, 2000.
[10] G. Bruns, “A Case Study in SafetyCritical Design,” Proc. Fourth Int'l Workshop ComputerAided Verification (CAV), pp. 220233, June 1992.
[11] R.E. Bryant, “GraphBased Algorithms for Boolean Function Manipulation,” IEEE Trans. Computers, vol. C35, no. 8, pp. 677691, 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. 5271, 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. 5062, Mar. 1996.
[17] A. Cribbens, “SolidState 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. 5456, Oct. 2005.
[19] A. David, J. Håkansson, K.G. Larsen, and P. Pettersson, “Minimal DBM Substraction,” Proc. 16th Nordic Workshop Programming Theory, pp. 1720, 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. 128142, Sept. 2006.
[21] D.L. Dill, “Timing Assumptions and Verification of Finitestate Concurrent Systems,” Proc. Workshop Automatic Verification Methods for Finite State Systems, pp. 197212, 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. 99122, July 1977.
[23] E. Fersman, L. Mokrushin, P. Pettersson, and Y. Wang, “Schedulability Analysis of FixedPriority Systems Using Timed Automata,” Theoretical Computer Science, vol. 354, no. 2, pp. 301317, Mar. 2006.
[24] G. Gössler and J. Sifakis, “Priority Systems,” Proc. Second Int'l Symp. Formal Methods for Components and Objects (FMCO), pp. 314329, Nov. 2003.
[25] P.A. Hsiung and S.W. Lin, “Model Checking Timed Systems with Priorities,” Proc. IEEE 11th Int'l Conf. Embedded and RealTime Computing Systems and Applications (RTCSA), pp. 539544, Aug. 2005.
[26] P.A. Hsiung and F. Wang, “A StateGraph Manipulator Tool for RealTime System Specification and Verification,” Proc. Fifth Int'l Conf. RealTime Computing Systems and Applications (RTCSA), Oct. 1998.
[27] K.G. Larsen, F. Larsson, P. Pettersson, and W. Yi, “Efficient Verification of RealTime Systems: Compact Data Structure and StateSpace Reduction,” Proc. IEEE 18th RealTime Systems Symp., pp. 1424, Dec. 1997.
[28] J.P. Lehoczky, L. Sha, and Y. Ding, “The Rate Monotonic Scheduling Algorithm: Exact Characterization and Average Case Behavior,” Proc. IEEE RealTime Systems Symp., pp. 166171, 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. 370384, Oct. 2005.
[30] C.L. Liu and J.W. Layland, “Scheduling Algorithms for Multiprogramming in a HardRealTime Environment,” J. ACM, vol. 20, no. 1, pp. 4661, 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. 337351, Apr. 1982.
[34] J. Sifakis, “The Compositional Specification of Timed Systems,” Proc. 11th Int'l Conf. ComputerAided Verification (CAV '99), pp. 27, July 1999.
[35] J. Sifakis, “Modeling RealTime Systems—Challenges and Work Directions,” Proc. First Int'l Workshop Embedded Software (EMSOFT), pp. 373389, Oct. 2001.
[36] F. Wang, “RED: ModelChecker for Timed Automata with ClockRestriction Diagram,” Proc. Workshop RealTime Tools, Aug. 2001.
[37] F. Wang and P.A. Hsiung, “Efficient and UserFriendly Verification,” IEEE Trans. Computers, vol. 51, no. 1, pp. 6183, Jan. 2002.
[38] S. Yovine, “Kronos: A Verification Tool for RealTime Systems,” Int'l J. Software Tools for Technology Transfer, vol. 1, nos. 1/2, pp. 123133, Oct. 1997.