This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Correctness Verification and Performance Analysis of Real-Time Systems Using Stochastic Preemptive Time Petri Nets
November 2005 (vol. 31 no. 11)
pp. 913-927
Time Petri Nets describe the state of a timed system through a marking and a set of clocks. If clocks take values in a dense domain, state space analysis must rely on equivalence classes. These support verification of logical sequencing and quantitative timing of events, but they are hard to be enriched with a stochastic characterization of nondeterminism necessary for performance and dependability evaluation. Casting clocks into a discrete domain overcomes the limitation, but raises a number of problems deriving from the intertwined effects of concurrency and timing. We present a discrete-time variant of Time Petri Nets, called stochastic preemptive Time Petri Nets, which provides a unified solution for the above problems through the adoption of a maximal step semantics in which the logical location evolves through the concurrent firing of transition sets. We propose an analysis technique, which integrates the enumeration of a succession relation among sets of timed states with the calculus of their probability distribution. This enables a joint approach to the evaluation of performance and dependability indexes as well as to the verification of sequencing and timeliness correctness. Expressive and analysis capabilities of the model are demonstrated with reference to a real-time digital control system.

[1] R.K. Ahuja, T.L. Magnanti, and J.B. Orlin, Network Flows. Prentice Hall, 1993.
[2] R. Alur and D.L. Dill, “Automata for Modeling Real-Time Systems,” Proc. 17th Int'l Colloquium on Automata, Languages, and Programming, 1990.
[3] R. Alur and T.A. Henzinger, “Logics and Models of Real-Time: A Survey,” Real-Time: Theory in Practice, 1992.
[4] T. Amnell, E. Fersman, L. Mokrushin, P. Pettersson, and W. Yi, “Times— A Tool for Modelling and Implementation of Embedded Systems,” Proc. Eighth Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, 2002.
[5] 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.
[6] 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, 1996.
[7] A. Benveniste, P. Caspi, S.A. Edwards, N. Halbwachs, P. Le Guernic, and R. DeSimone, “The Synchronous Languages 12 Years Later,” Proc. IEEE, vol. 91, no. 1, pp. 64-83, Jan. 2003.
[8] G. Berry and G. Gonthier, “The ESTEREL Synchronous Programming Language: Design, Semantics, Implementation,” Science of Computer Programming, vol. 19, no. 2, pp. 87-152, 1992.
[9] 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.
[10] B. Berthomieu and M. Menasche, “An Enumerative Approach for Analyzing Time Petri Nets,” Proc. IFIP Congress, Sept. 1983.
[11] B. Berthomieu, P.-O. Ribet, and F. Vernadat, “The Tool TINA-Construction of Abstract State Spaces for Petri Nets and Time Petri Nets,” Int'l J. Production Research, 2004.
[12] A. Bobbio and A. Horvath, “Petri Nets with Discrete Phase Type Timing: A Bridge between Stochastic and Functional Analysis,” Electronic Notes in Theoretical Computer Science, vol. 52, no. 3, 2001.
[13] A. Bobbio, A. Puliafito, M. Scarpa, and M. Telek, “WebSPN: Non-Markovian Stochastic Petri Net Tool,” Proc. 18th Int'l Conf. Application and Theory of Petri Nets, June 1997.
[14] A. Bobbio, A. Puliafito, M. Telek, and K. Trivedi, “Recent Developments in Non-Markovian Stochastic Petri Nets,” J. Systems Circuits and Computers, vol. 8, no. 1, pp. 119-158, 1998.
[15] A. Bobbio and M. Scarpa, “Kronecker Representation of Stochastic Petri Nets with Discrete PH Distributions,” Proc. Third IEEE Ann. Int'l Computer Performance and Dependability Symp. (IPDS '98), Sept. 1998.
[16] R. Bruni, J. Meseguer, U. Montanari, and V. Sassone, “A Comparison of Petri Net Semantics under the Collective Token Philosophy,” Proc. Asian Computing Science Conf. (ASIAN), pp. 225-244, 1998.
[17] G. Bucci and E. Vicario, “Compositional Validation of Time-Critical Systems Using Communicating Time Petri Nets,” IEEE Trans. Software Eng., vol. 21, no. 12, Dec. 1995.
[18] G. Bucci, A. Fedeli, L. Sassoli, and E. Vicario, “Modeling Flexible Real-Time Systems with Preemptive Time Petri Nets,” Proc. 15th Euromicro Conf. Real-Time Systems (ECRTS03), July 2003.
[19] G. Bucci, L. Sassoli, and E. Vicario, “A Discrete Time Model for Performance Evaluation and Correctness Verification of Real-Time Systems,” Proc. 10th Int'l Workshop Petri Nets and Performance Models (PNPM '03), Sept. 2003.
[20] G. Bucci, A. Fedeli, L. Sassoli, and E. Vicario, “Timed State Space Analysis of Real-Time Preemptive Systems,” IEEE Trans. Software Eng., vol. 30, no. 2, pp. 97-111, Feb. 2004.
[21] G. Bucci, L. Sassoli, and E. Vicario, “Oris: A Tool for State Space Analysis of Real-Time Preemptive Systems,” Proc. First Int'l Conf. the Quantitative Evaluation of Systems (QEST '04), Sept. 2004.
[22] G. Bucci, R. Piovosi, L. Sassoli, and E. Vicario, “Introducing Probability within State Class Analysis of Dense-Time-Dependent Systems,” Proc. Int'l Conf. the Quantitative Evaluation of Systems (QEST '05), Sept. 2005.
[23] P. Buchholz and I.V. Tarasyuk, “Net and Algebraic Approaches to Probabilistic Modeling,” Joint Novosibirsk Computing Center and Institute of Informatics Systems Bulletin, Series Computer Science, pp. 31-64, 2001.
[24] G. Buttazzo, Hard Real-Time Computing Systems. Norwell, Mass.: Kluwer, 1997.
[25] M. Caccamo, L. Abeni, G.C. Buttazzo, and G. Lipari, “Elastic Scheduling for Flexible Workload Management,” IEEE Trans. Computers, 2002.
[26] F. Cassez and K.G. Larsen, “The Impressive Power of Stopwatches,” Proc. 11th Int'l Conf. Concurrency Theory, pp. 138-152, Aug. 2000.
[27] A. Cervin, “Improved Scheduling of Control Tasks,” Proc. 11th Euromicro Conf. Real-Time Systems, pp. 4-10, June 1999.
[28] A. Cervin, “Merging Real-Time and Control Theory for Improving the Performance of Embedded Control Systems,” research report, Sept. 2004.
[29] A. Cervin, B. Lincoln, J. Eker, K.E. Ârzén, and G. Buttazzo, “The Jitter Margin and Its Application in the Design of Real-Time Control Systems,” Proc. 10th Int'l Conf. Real-Time and Embedded Computing Systems and Applications (RTCSA), Aug. 2004.
[30] G. Chiola, M. AjmoneMarsan, G. Balbo, and G. Conte, “Generalized Stochastic Petri Nets: A Definition at the Net Level and Its Implications,” IEEE Trans. Software Eng., Feb. 1993.
[31] G. Ciardo, “Discrete Time Markovian Stochastic Petri Nets,” Proc. Second Workshop Numerical Solution of Markovian Chains, 1995.
[32] G. Ciardo and R. Zijal, “Well Defined Sthocastic Petri Nets” Proc. Fourth Int'l Workshop Modeling Analysis and Simulation of Computer and Telecomunication Systems (MASCOTS '96), 1996.
[33] G. Ciardo, R. Zijal, and G. Hommel, “Discrete Deterministic and Stochastic Petri Nets” Measurement, Modeling, and Valuation of Computer and Communication-Systems, pp. 103-117, Sept. 1997.
[34] E.M. Clarke, E.A. Emerson, and A. Sistla, “Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications,” ACM Trans. Programming Language, vol. 8, no. 2, pp. 244-263, 1986.
[35] C. Courcoubetis and S. Tripakis, “Probabilistic Model Checking: Formalisms and Algorithms for Discrete and Real-Time Systems,” Verification of Digital and Hybrid Systems, pp. 183-219, 2000.
[36] C. Daws, A. Olivero, S. Tripakis, and S. Yovine, “The Tool KRONOS,” Hybrid Systems III, 1996.
[37] R. De Nicola and F.W. Van Draager, “Action versus State Based Logics for Transition Systems,” Proc. LITP Spring School on Theoretical Computer Science, pp. 407-419, 1990.
[38] E. Fersman, P. Pettersson, and W. Yi, “Timed Automata with Asynchronous Processes: Schedulability and Decidability,” Tools and Algorithms for Construction and Analysis of Systems, 2002.
[39] K. Goseva-Popstojanova and K.S. Trivedi, “Stochastic Modeling Formalisms for Dependability, Performance and Performability,” Performance Evaluation— Origins and Directions, pp. 385-404, 2000.
[40] D. Harel and A. Pnueli, “On the Development of Reactive Systems,” Logics and Models of Concurrent Systems (NATO), 1985.
[41] A. Horvath, A. Puliafito, M. Scarpa, and M. Telek, “Analysis and Evaluation of NonMarkovian Stochastic Petri Nets,” Proc. 11th Int'l Conf. Computer Performance Evaluation (TOOLS), pp. 171-187, 2000.
[42] K. Jay, L. Kevin, and B. Kenny, “Building Flexible Real-Time System Using the Flex Language,” Computer, 1991.
[43] I. Lee, P. Bremond-Gregoire, and R. Gerber, “A Process Algebraic Approach to the Specification and Analysis of Resource Bound Real-Time Systems,” Proc. IEEE, vol. 82, no. 1, pp. 158-171, Jan. 1994.
[44] I. Lee, J.-Y. Choi, H.-H. Kwak, A. Philippou, and O. Sokolsky, “A Family of Resource-Bound Real-Time Process Algebras,” Proc. 21st Int'l Conf. Formal Techniques for Networked and Distributed Systems (FORTE '01), Aug. 2001.
[45] M. Ajmone Marsan, G. Balbo, and G. Conte, “A Class of Generalized Stochastic Petri Nets for the Performance Evaluation of Multiprocessor Systems,” ACM Trans. Computer Systems, vol. 2, no. 2, pp. 93-122, May 1984.
[46] J. McManis and P. Varaiya, “Suspension Automata: A Decidable Class of Hybrid Automata,” Proc. Computer Aided Verification: Sixth Int'l Conf. (CAV '94), June 1994.
[47] P. Merlin and D.J. Farber, “Recoverability of Communication Protocols,” IEEE Trans. Comm., vol. 24, no. 9 Sept. 1976.
[48] X. Nicollin, J. Sifakis, and S. Yovine, “Compiling Real-Time Specifications into Extended Automata,” IEEE Trans. Software Eng., vol. 18, no. 9, Sept. 1992.
[49] D. Lime and O.H. Roux, “Expressiveness and Analysis of Scheduling Extended Time Petri Nets,” Proc. Fifth IFAC Conf. Fieldbus and Their Applications (FET 2003), July 2003.
[50] O. Sokolsky, I. Lee, and H. Ben-Abdallah, “Specification and Analysis of Real-Time Systems with PARAGON,” Annals of Software Eng., vol. 7 1999.
[51] E. Smith, “On the Border of Causality: Contact and Confusion,” Theoretical Computer Science, vol. 153, pp. 275-270, 1996.
[52] J.A. Stankovic and K. Ramamritham, “What Is Predictability for Real-Time Systems,” J. Real-time Systems, vol. 2 Dec. 1990.
[53] A.S. Tanenbaum, Modern Operating Systems. Prentice Hall, 2001.
[54] E. Teruel, G. Franceschinis, and M. DePierro, “Well Defined Generalized Stochastic Petri Nets: A Net Level Method to Specify Priorities,” IEEE Trans. Software Eng., vol. 29, Nov. 2003.
[55] M.Y. Vardi, “Automatic Verification of Probabilistic Concurrent Finite-State Programs,” Proc. Symp. Foundations of Computer Science (FOCS '85), pp. 327-338, 1985.
[56] E. Vicario, “Static Analysis and Dynamic Steering of Time Dependent Systems Using Time Petri Nets,” IEEE Trans. Software Eng., Aug. 2001.
[57] B. Wittenmark and N. Trngren, “Timing Problems in Real-Time Control Systems,” Proc. Am. Control Conf., 1995.
[58] R. Zijal, “Discrete Time Deterministic and Stochastic Petri Nets,” Proc. Int'l Workshop Quality of Comm.-Based Systems, pp. 123-136, 1994.
[59] A. Zimmermann, J. Freiheit, and G. Hommel, “Discrete Time Stochastic Petri Nets for Modeling and Evaluation of Real-Time Systems,” Proc. Int'l Parallel and Distributed Processing Symp., 2001.

Index Terms:
Index Terms- Real-time reactive systems, preemptive scheduling, correctness verification, performance and dependability evaluation, discrete time, maximal step semantics, confusion, well definedness, stochastic preemptive Time Petri nets.
Citation:
Giacomo Bucci, Luigi Sassoli, Enrico Vicario, "Correctness Verification and Performance Analysis of Real-Time Systems Using Stochastic Preemptive Time Petri Nets," IEEE Transactions on Software Engineering, vol. 31, no. 11, pp. 913-927, Nov. 2005, doi:10.1109/TSE.2005.122
Usage of this product signifies your acceptance of the Terms of Use.