This Article 
 Bibliographic References 
 Add to: 
Timed State Space Analysis of Real-Time Preemptive Systems
February 2004 (vol. 30 no. 2)
pp. 97-111

Abstract—A modeling notation is introduced which extends Time Petri Nets with an additional mechanism of resource assignment making the progress of timed transitions be dependent on the availability of a set of preemptable resources. The resulting notation, which we call Preemptive Time Petri Nets, permits natural description of complex real-time systems running under preemptive scheduling, with periodic, sporadic, and one-shot processes, with nondeterministic execution times, with semaphore synchronizations and precedence relations deriving from internal task sequentialization and from interprocess communication, running on multiple processors. A state space analysis technique is presented which supports the validation of Preemptive Time Petri Net models, combining tight schedulability analysis with exhaustive verification of the correctness of logical sequencing. The analysis technique partitions the state space in equivalence classes in which timing constraints are represented in the form of Difference Bounds Matrixes. This permits it to maintain a polynomial complexity in the representation and derivation of state classes, but it does not tightly encompass the constraints deriving from preemptive behavior, thus producing an enlarged representation of the state space. False behaviors deriving from the approximation can be cleaned-up through an algorithm which provides a necessary and sufficient condition for the feasibility of a behavior along with a tight estimation of its timing profile.

[1] R.K. Ahuja, T.L. Magnanti, and J.B. Orlin, Network Flows. Prentice Hall, 1993.
[2] K. Altisen, G. Goessler, and J. Sifakis, Scheduler Modeling Based on the Controller Synthesis Paradigm Real Time Systems, vol. 23, pp. 55-84, 2002.
[3] R. Alur and D.L. Dill, Automata for Modeling Real-Time Systems Proc. 17th Int'l Colloquium on Automata, Languages, and Programming, 1990.
[4] R. Alur, T.A. Henzinger, and P.-H. Ho, “Automatic Symbolic Verification of Embedded Systems,” IEEE Trans. Software Eng., vol. 22, no. 3, Mar. 1996.
[5] T. Amnell, E. Fersman, L. Mokrushin, P. Pettersson, and W. Yi, Times A Tool for Modelling and Implementation of Embedded Systems Lecture Notes in Computer Science, vol. 2280, 2002.
[6] B. Andersson and J. Jonsson, Preemptive Multiprocessor Scheduling Anomalies Proc. Int'l Parallel (and Distributed) Processing Symp., pp. 12-19, 2002.
[7] G.S. Avrunin, J.C. Corbett, L.K. Dillon, and J.C. Wileden, Automated Derivation of Time Bounds in Uniprocessor Concurrent Systems IEEE Trans. Software Eng., vol. 20, no. 9, 1994.
[8] H. Ben-Abdallah, J.-Y. Choi, D. Clarke, Y.-S. Kim, I. Lee, and H.-L. Xie, A Process Algebraic Approach to the Schedulability Analysis of Real Time Systems Real Time Systems, vol. 15, no. 3, pp. 189-219, 1998.
[9] J. Bengtsson, K.G. Larsen, F. Larsson, P. Pettersson, and W. Yi, UPPAAL: A Tool-Suite for Automatic Verification of Real-Time Systems Hybrid Systems III, R. Alur, T.A. Henzinger, E.D. Sontag, eds., 1996.
[10] B. Berthomieu and M. Diaz, “Modeling and Verification of Time Dependent Systems Using Time Petri Nets,” IEEE Trans. Software Eng., vol. 17, no. 3, Mar. 1991.
[11] B. Berthomieu and M. Menasche, An Enumerative Approach for Analyzing Time Petri Nets Proc. IFIP Congress, Sept. 1983.
[12] A. Bobbio, A. Puliafito, and M. Telek, “A Modeling Framework to Implement Combined Preemption Policies in MRSPNs,” IEEE Trans. Software Eng., vol. 26, no. 1, pp. 36-54, Jan. 2000.
[13] G. Bucci and E. Vicario, “Compositional Validation of Time-Critical Systems Using Communicating Time Petri Nets,” IEEE Trans. Software Eng., vol. 21, no. 12, pp. 969–992, Dec. 1995.
[14] F. Cassez and K.G. Larsen, The Impressive Power of Stopwatches Lecture Notes in Computer Science, vol. 1877, pp. 138-152, Aug. 2000.
[15] J.C. Corbett, “Timing Analysis of Ada Tasking Programs,” IEEE Trans. Software Eng., vol. 22, no. 7, pp. 461-483, July 1996.
[16] C. Daws, A. Olivero, S. Tripakis, and S. Yovine, The Tool KRONOS Hybrid Systems III, R. Alur, T.A. Henzinger, E.D. Sontag, eds., 1996.
[17] D. Dill, Timing Assumptions and Verification of Finite-State Concurrent Systems Proc. CAV Methods for Finite State Systems Conf., 1989.
[18] E. Fersman, P. Pettersson, and W. Yi, Timed Automata with Asynchronous Processes: Schedulability and Decidability Lecture Notes in Computer Science, vol. 2280, 2002.
[19] M.G. Harbour, M.H. Klein, and J.P. Lehoczky, “Timing Analysis for Fixed Priority Scheduling of Hard Real Time Systems,” IEEE Trans. Software Eng., vol. 20, no. 1, pp. 13-28, Jan. 1994.
[20] C.L. Liu and J.W. Layland, Scheduling Algorithms for Multiprogramming in a Hard-Real-Time Environment J. the ACM, vol. 20, no. 1, 1973.
[21] J. McManis and P. Varaiya, Suspension Automata: A Decidable Class of Hybrid Automata Proc. Computer Aided Verification: Sixth Int'l Conf., June 1994.
[22] P. Merlin and D.J. Farber, Recoverability of Communication Protocols IEEE Trans. Comm., vol. 24, no. 9, Sept. 1976.
[23] T. Murata, “Petri Nets: Properties, Analysis and Application,” Proc. IEEE, vol. 77, no. 4, 1989.
[24] X. Nicollin, J. Sifakis, and S. Yovine, “Compiling Real-Time Specifications into Extended Automata,” IEEE Trans. Software Eng., vol. 18, no. 9, pp. 794-804, Sept. 1992.
[25] J.L. Peterson, Petri Nets ACM Computing Surveys, vol. 9, no. 3, Sept. 1977.
[26] K. Ramamritham and J.A. Stankovic, “Scheduling Algorithms and Operating System Support for Real Time Systems,” Proc. IEEE, vol. 82, no. 1, Jan. 1994.
[27] L. Sha, R. Rajkuma, and J.P. Lehoczky, "Priority Inheritance Protocols: An Approach to Real-Time Synchronization," IEEE Trans. Computers, vol. 39, no. 9, pp. 1,175-1,185, Sept. 1990.
[28] L. Sha, R. Rajkumar, and S.S. Sathaye, Generalized Rate Monotonic Scheduling Theory: A Framework for Developing Real Time Systems Proc. IEEE, vol. 82, no. 1, 1994.
[29] J. Sun, M.K. Gardner, and J.W.S. Liu, “Bounding Completion Times of Jobs with Arbitrary Release Times, Variable Execution Times, and Resource Sharing,” IEEE Trans. Software Eng., vol. 23, no. 10, Oct. 1997.
[30] E. Vicario, Static Analysis and Dynamic Steering of Time Dependent Systems Using Time Petri Nets IEEE Trans. Software Eng., Aug. 2001.
[31] J. Xu and D.L. Parnas, "On Satisfying Timing Constraints in Hard Real-Time Systems," IEEE Trans. Software Eng., Vol. 19, No. 1, Jan. 1993, pp. 70-84.
[32] R.M. Fricks, A. Puliafito, M. Telek, and K. Trivedi, Applications of Non-Markovian Stochastic Petri Nets Performance Evaluation Rev., vol. 26, no. 2, 1998.
[33] W.M. Zuberek, M-Timed Petri Nets, Priorities, Preemptions, and Performance Evaluation of Systems Advances in Petri Nets 1985, 1986.
[34] W.M. Zuberek, Preemptive D-Timed Petri Nets, Timeouts, Modelling and Analysis of Communication Protocols Proc. IEEE INFOCOM Conf. Computer Comm.: Global Networks, pp. 721-730, 1987.

Index Terms:
Hard real-time systems, reactive systems, preemptive scheduling, interprocess communication, nondeterministic time parameters, multiprocessor schedulability, timeliness predictability, state space analysis, Preemptive Time Petri Nets.
Giacomo Bucci, Andrea Fedeli, Luigi Sassoli, Enrico Vicario, "Timed State Space Analysis of Real-Time Preemptive Systems," IEEE Transactions on Software Engineering, vol. 30, no. 2, pp. 97-111, Feb. 2004, doi:10.1109/TSE.2004.1265815
Usage of this product signifies your acceptance of the Terms of Use.