The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.05 - September/October (2009 vol.35)
pp: 703-719
Enrico Vicario , Università di Firenze, Firenze
Luigi Sassoli , Università di Firenze, Firenze
Laura Carnevali , Università di Firenze, Firenze
ABSTRACT
In the verification of reactive systems with nondeterministic densely valued temporal parameters, the state-space can be covered through equivalence classes, each composed of a discrete logical location and a dense variety of clock valuations encoded as a Difference Bounds Matrix (DBM). The reachability relation among such classes enables qualitative verification of properties pertaining events ordering and stimulus/response deadlines, but it does not provide any measure of probability for feasible behaviors. We extend DBM equivalence classes with a density-function which provides a measure for the probability of individual states. To this end, we extend Time Petri Nets by associating a probability density-function to the static firing interval of each nondeterministic transition. We then explain how this stochastic information induces a probability distribution for the states contained within a DBM class and how this probability evolves in the enumeration of the reachability relation among classes. This enables the construction of a stochastic transition system which supports correctness verification based on the theory of TPNs, provides a measure of probability for each feasible run, enables steady-state analysis based on Markov Renewal Theory. In so doing, we provide a means to identify feasible behaviors and to associate them with a measure of probability in models with multiple concurrent generally distributed nondeterministic timers.
INDEX TERMS
Correctness verification, performance and dependability evaluation, stochastic Time Petri nets, non-Markovian Stochastic Petri Nets, dense-time state-space analysis, Difference Bounds Matrix, Markov Renewal Theory.
CITATION
Enrico Vicario, Luigi Sassoli, Laura Carnevali, "Using Stochastic State Classes in Quantitative Evaluation of Dense-Time Reactive Systems", IEEE Transactions on Software Engineering, vol.35, no. 5, pp. 703-719, September/October 2009, doi:10.1109/TSE.2009.36
REFERENCES
[1] M.M. Ajmone, 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, pp. 93-122, 1984.
[2] M.M. Ajmone and G. Chiola, “On Petri Nets with Deterministic and Exponentially Distributed Firing Times,” Lecture Notes in Computer Science, vol. 266, pp. 132-145, 1987.
[3] R. Alur, C. Courcoubetis, and D. Dill, “Model-Checking for Real-Time Systems,” Proc. Fifth Symp. Logic in Computer Science, June 1990.
[4] R. Alur and D.L. Dill, “Automata for Modeling Real-Time Systems,” Proc. 17th Int'l Colloquium on Automata, Languages, and Programming, 1990.
[5] R. Alur, T.A. Henzinger, and P.H. Ho, “Automatic Symbolic Verification of Embedded Systems,” IEEE Trans. Software Eng., vol. 22, no. 3, pp. 181-201, Mar. 1996.
[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, Springer, 1996.
[7] B. Berthomieu and M. Diaz, “Modeling and Verification of Time Dependent Systems Using Time Petri Nets,” IEEE Trans. Software Eng., vol. 17, no. 3, pp. 259-273, Mar. 1991.
[8] B. Berthomieu and M. Menasche, “An Enumerative Approach for Analyzing Time Petri Nets,” Proc. Int'l Federation for Information Processing Congress 1983, R.E.A. Mason, ed., vol. 9, pp. 41-46, 1983.
[9] 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, vol. 42, no. 14, pp. 2741-2756, 2004.
[10] A. Bobbio, A. Puliafito, and M. Telek, “A Modelling Framework to Implement Preemption Policies in Non-Markovian SPNs,” IEEE Trans. Software Eng., vol. 26, no. 1, pp. 36-54, Jan. 2000.
[11] A. Bobbio and M. Telek, “A Benchmark for PH Estimation Algorithms: Result for Acyclic-PH,” Stochastic Models, vol. 10, pp.661-677, 1994.
[12] A. Bobbio and M. Telek, “Markov Regenerative SPN with Non-Overlapping Activity Cycles,” Proc. Int'l Computer Performance and Dependability Symp., pp. 124-133, 1995.
[13] G. Bucci, R. Piovosi, L. Sassoli, and E. Vicario, “Introducing Probability within State Class Analysis of Dense Time Dependent Systems,” Proc. Second Int'l Conf. Quantitative Evaluation of Systems, Sept. 2005.
[14] G. Bucci, L. Sassoli, and E. Vicario, “Oris: A Tool for State Space Analysis of Real-Time Preemptive Systems,” Proc. First Int'l Conf. Quantitative Evaluation of Systems, 2004.
[15] H. Choi, V.G. Kulkarni, and K. Trivedi, “Markov Regenerative Stochastic Petri Nets,” Performance Evaluation, vol. 20, pp. 337-357, 1994.
[16] G. Ciardo, R. German, and C. Lindemann, “A Characterization of the Stochastic Process Underlying a Stochastic Petri Net,” IEEE Trans. Software Eng., vol. 20, no. 7, pp. 506-515, July 1994.
[17] G. Ciardo, J. Muppala, and K.S. Trivedi, “SPNP: Stochastic Petri Net Package,” Proc. IEEE Int'l Workshop Petri Nets and Performance Models, pp. 142-151, 1989.
[18] C. Daws, A. Olivero, S. Tripakis, and S. Yovine, “The Tool KRONOS,” Hybrid Systems III, Springer, 1995.
[19] D. Dill, “Timing Assumptions and Verification of Finite-State Concurrent Systems,” Proc. Workshop Computer Aided Verification Methods for Finite State Systems, 1989.
[20] G. Gardey, D. Lime, M. Magnin, and O. Roux, “Roméo: A Tool for Analyzing Time Petri Nets,” Proc. 17th Int'l Conf. Computer Aided Verification, 2005.
[21] 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.
[22] G. Buttazzo, Hard Real-Time Computing Systems. Springer, 2005.
[23] R. German, Performance Analysis of Communication Systems with Non-Markovian Stochastic Petri Nets. John Wiley & Sons, 2000.
[24] R. German and C. Lindemann, “Analysis of Stochastic Petri Nets by the Method of Supplementary Variables,” Performance Evaluation, vol. 20, pp. 317-335, 1994.
[25] R. German and M. Telek, “Formal Relation of Markov Renewal Theory and Supplementary Variables in the Analysis of Stochastic Petri Nets,” Proc. Eighth Int'l Workshop Petri Nets and Performance Models, pp. 64-73, 1999.
[26] D. Harel and A. Pnueli, “On the Development of Reactive Systems,” Logics and Models of Concurrent Systems, Springer, 1985.
[27] ISO/IEC, International Standard 9126:2001, Information Technology—SW Product Quality—Part 1: Quality Model, 2001.
[28] W.-T. Jong, Y.-S. Shiau, Y.-J. Horng, H.-H. Chen, and S.-M. Chen, “Temporal Knowledge Representation and Reasoning Techniques Using Time Petri Nets,” IEEE Trans. Systems, Man, and Cybernetics, vol. 29, no. 4, pp. 541-545, Aug. 1999.
[29] L. Carnevali, L. Grassi, and E. Vicario, “State-Density Functions over DBM Domains in the Analysis of Non-Markovian Models,” IEEE Trans. Software Eng., vol. 35, no. 2, pp. 178-194, Mar./Apr. 2009.
[30] D. Lime and O.H. Roux, “Expressiveness and Analysis of Scheduling Extended Time Petri Nets,” Proc. Fifth Int'l Federation of Automatic Control Conf. Fieldbus and Their Applications, 2003.
[31] C. Lindemann and G.S. Schedler, “Numerical Analysis of Deterministic and Stochastic Petri Nets with Concurrent Deterministic Transitions,” Performance Evaluation, vols. 27/28, pp. 565-582, 1996.
[32] C. Lindemann and A. Thuemmler, “Transient Analysis of Deterministic and Stochastic Petri Nets with Concurrent Deterministic Transitions,” Performance Evaluation, vols. 36/37, pp. 35-54, 1999.
[33] M.K. Molloy, “Discrete Time Stochastic Petri Nets,” IEEE Trans. Software Eng., vol. 11, no. 4, pp. 417-423, Apr. 1985.
[34] M.F. Neuts, Matrix Geometric Solutions in Stochastic Models. Johns Hopkins Univ. Press, 1981.
[35] W. Penczek and A. Polrola, “Specification and Model Checking of Temporal Properties in Time Petri Nets and Timed Automata,” Proc. 25th Int'l Conf. Application and Theory of Petri Nets, June 2004.
[36] K.G. Popstojanova and K.S. Trivedi, “Stochastic Modeling Formalisms for Dependability, Performance and Performability,” Performance Evaluation—Origins and Directions, pp. 385-404, Springer, 2000.
[37] L. Sassoli and E. Vicario, “Analysis of Real Time Systems through the Oris tool,” Proc. Fourth Int'l Conf. Quantitative Evaluation of Systems, Sept. 2006.
[38] L. Sassoli and E. Vicario, “Close Form Derivation of State-Density Functions over DBM Domains in the Analysis of Non-Markovian Models,” Proc. Fifth Int'l Conf. Quantitative Evaluation of Systems, Sept. 2007.
[39] J.A. Stankovic and K. Ramamritham, “What Is Predictability for Real Time Systems,” J. Real Time Systems, vol. 2, pp. 247-254, 1990.
[40] M. Telek and A. Horvarth, “Supplementary Variable Approach Applied to the Transient Analysis of Age-MRSPNs,” Proc. Int'l Performance and Dependability Symp., pp. 44-51, 1998.
[41] E. Vicario, “Static Analysis and Dynamic Steering of Time Dependent Systems Using Time Petri Nets,” IEEE Trans. Software Eng., vol. 27, no. 8, pp. 728-748, Aug. 2001.
[42] WolframResearch “Mathemathica 5.2,” www.wolfram.com, 2009.
[43] D. Xu, X. He, and Y. Deng, “Compositional Schedulability Analysis of Real-Time Systems Using Time Petri Nets,” IEEE Trans. Software Eng., vol. 28, no. 10, pp. 984-996, Oct. 2002.
5 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool