Subscribe

Issue No.02 - March/April (2009 vol.35)

pp: 178-194

Laura Carnevali , Università di Firenze, Firenze

Leonardo Grassi , Università di Firenze, Firenze

Enrico Vicario , Università di Firenze, Firenze

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TSE.2008.101

ABSTRACT

Quantitative evaluation of models with generally-distributed transitions requires analysis of non-Markovian processes that may be not isomorphic to their underlying untimed models and may include any number of concurrent non-exponential timers. The analysis of stochastic Time Petri Nets copes with the problem by covering the state space with stochastic-classes, which extend Difference Bounds Matrices (DBM) with a state probability density function. We show that the state-density function accepts a continuous piecewise representation over a partition in DBM-shaped sub-domains. We then develop a closed-form symbolic calculus of state-density functions assuming that model transitions have expolynomial distributions. The calculus shows that within each sub-domain the state-density function is a multivariate expolynomial function and makes explicit how this form evolves through subsequent transitions. This enables an efficient implementation of the analysis process and provides the formal basis that supports introduction of an approximate analysis based on Bernstein Polynomials. The approximation attacks practical and theoretical limits in the applicability of stochastic state-classes, and devises a new approach to the analysis of non Markovian models, relying on approximations in the state space rather than in the structure of the model.

INDEX TERMS

Software Engineering, Tools, Validation, Software and System Safety, Software/Program Verification, Formal methods, Reliability, Automata, Parallelism and concurrency, Approximation, Markov processes, Renewal theory, Stochastic processes

CITATION

Laura Carnevali, Leonardo Grassi, Enrico Vicario, "State-Density Functions over DBM Domains in the Analysis of Non-Markovian Models",

*IEEE Transactions on Software Engineering*, vol.35, no. 2, pp. 178-194, March/April 2009, doi:10.1109/TSE.2008.101REFERENCES

- [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, 1984.- [2] R. Alur, C. Courcoubetis, and D. Dill, “Model-Checking for Real-Time Systems,”
Proc. Fifth Symp. Logic in Computer Science, June 1990.- [3] R. Alur and D.L. Dill, “Automata for Modeling Real-Time Systems,”
Proc. 17th Int'l Colloquium Automata, Languages and, Programming, 1990.- [4] G. Behrmann, A. David, and K.G. Larsen, “A Tutorial on uppaal,”
Formal Methods for the Design of Real-Time Systems: Proc. Fourth Int'l School Formal Methods for the Design of Computer, Comm., and SW Systems, pp.200-236, Sept. 2004.- [5] G. Behrmann, K.G. Larsen, J. Pearson, C. Weise, and W. Yi, “Efficient Timed Reachability Analysis Using Clock Difference Diagrams,”
Proc. 11th Int'l Conf. Computer Aided Verification, 1999.- [7] B. Berthomieu and M. Menasche, “An Enumerative Approach for Analyzing Time Petri Nets,”
Information Processing: Proc. IFIP Congress 1983, R.E.A. Mason, ed., vol.9, pp.41-46, 1983.- [8] 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, 2004.- [11] 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. Quantum Evaluation of Systems, Sept. 2005.- [12] G. Bucci, L. Sassoli, and E. Vicario, “Oris: A Tool for State Space Analysis of Real-Time Preemptive Systems,”
Proc. First Int'l Conf. Quantum Evaluation of Systems, 2004.- [13] L. Carnevali, L. Sassoli, and E. Vicario, “Using Stochastic State Classes in Quantitative Evaluation of Dense-Time Reactive Systems,”
IEEE Trans. Software Eng., accepted for publication. - [14] F. Cassez and K. Larsen,
The Impressive Power of Stopwatches, Aug. 2000.- [17] G. Ciardo, J. Muppala, and K.S. Trivedi, “SPNP: Stochastic Petri Net Package,”
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,”
Proc. Hybrid Systems III, 1995.- [19] D. Dill, “Timing Assumptions and Verification of Finite-State Concurrent Systems,”
Proc. Workshop Computer Aided Verification Methods for Finite State Systems, 1989.- [21] G. Gardey, D. Lime, M. Magnin, and O. Roux, “Romeo: A Tool for Analyzing Time Petri Nets,”
Proc. 17th Int'l Conf. Computer Aided Verification, 2005.- [22] R. German, “Transient Analysis of Deterministic and Stochastic Petri Nets by the Method of Supplementary Variables,”
Proc. Third Int'l Workshop Modeling, Analysis, and Simulation of Computer and Telecomm. Systems, 1995.- [26] G. Lorentz,
Bernstein Polynomials. Univ. of Toronto Press, 1953.- [28] P. Merlin and D. Farber, “Recoverability of Communication Protocols,”
IEEE Trans. Comm., vol. 24, no. 9, 1976.- [30] M.F. Neuts,
Matrix Geometric Solutions in Stochastic Models. Johns Hopkins Univ. Press, 1981.- [31] 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.- [32] L. Sassoli and E. Vicario, “Analysis of Real Time Systems Through the Oris Tool,”
Proc. Fourth Int'l Conf. Quantum Evaluation of Systems, Sept. 2006.- [33] 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. Quantum Evaluation of Systems, Sept. 2007.- [37] 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.- [38] WolframResearch, Mathemathica 5.2, www.wolfram.com, 2009.
- [39] A. Zimmermann, J. Freiheit, R. German, and G. Hommel, “Petri Net Modelling and Performability Evaluation with TimeNET 3.0,”
Proc. 11th Int'l Conf. Modelling Techniques and Tools for Computer Perfermonce Evaluation, pp.188-202, 2000. |