This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
State-Density Functions over DBM Domains in the Analysis of Non-Markovian Models
March/April 2009 (vol. 35 no. 2)
pp. 178-194
ASCII Text
x 
 
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.
 
 
BibTex
x
 
@article{ 10.1109/TSE.2008.101,
author = {Laura Carnevali and Leonardo Grassi and Enrico Vicario},
title = {State-Density Functions over DBM Domains in the Analysis of Non-Markovian Models},
journal ={IEEE Transactions on Software Engineering},
volume = {35},
number = {2},
issn = {0098-5589},
year = {2009},
pages = {178-194},
doi = {http://doi.ieeecomputersociety.org/10.1109/TSE.2008.101},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - JOUR
JO - IEEE Transactions on Software Engineering
TI - State-Density Functions over DBM Domains in the Analysis of Non-Markovian Models
IS - 2
SN - 0098-5589
SP178
EP194
EPD - 178-194
A1 - Laura Carnevali,
A1 - Leonardo Grassi,
A1 - Enrico Vicario,
PY - 2009
KW - Software Engineering
KW - Tools
KW - Validation
KW - Software and System Safety
KW - Software/Program Verification
KW - Formal methods
KW - Reliability
KW - Automata
KW - Parallelism and concurrency
KW - Approximation
KW - Markov processes
KW - Renewal theory
KW - Stochastic processes
VL - 35
JA - IEEE Transactions on Software Engineering
ER -
 
Laura Carnevali, Università di Firenze, Firenze
Leonardo Grassi, Università di Firenze, Firenze
Enrico Vicario, Università di Firenze, Firenze
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.

[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.
[6] 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.
[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.
[9] A. Bobbio and M. Telek, “A Benchmark for PH Estimation Algorithms: Result for Acyclic-PH,” Stochastic Models, vol. 10, pp.661-677, 1994.
[10] 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.
[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.
[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,” 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.
[20] A. Feldmann and W. Whitt, “Fitting Mixtures of Exponentials to Long-Tail Distributions to Analyze Network Performance Models,” Performance Evaluation, vol. 31, nos.3-4, pp.245-279, 1998.
[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.
[23] 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.
[24] C. Lindemann and G.S. Shedler, “Numerical Analysis of Deterministic and Stochastic Petri Nets with Concurrent Deterministic Transitions,” Performance Evaluation, vols. 27/28, pp. 565-582, 1996.
[25] 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.
[26] G. Lorentz, Bernstein Polynomials. Univ. of Toronto Press, 1953.
[27] S. Manolache, P. Eles, and Z. Peng, “Schedulability Analysis of Multiprocessor Real-Time Applications with Stochastic Task Execution Times,” Proc. 20th Int'l Conf. Computer Aided Design, pp.699-706, Nov. 2002.
[28] P. Merlin and D. Farber, “Recoverability of Communication Protocols,” IEEE Trans. Comm., vol. 24, no. 9, 1976.
[29] M.K. Molloy, “Discrete Time Stochastic Petri Nets,” IEEE Trans. Software Eng., vol. 11, no. 4, pp. 417-723, Apr. 1985.
[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.
[34] T. Sauer, “Multivariate Bernstein Polynomials and Convexity,” Computer Aided Geometric Design, vol. 8, no. 6, pp.465-478, 1991.
[35] 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.
[36] 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, no. 11 pp.962-973, Nov. 2003.
[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.

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.101
Usage of this product signifies your acceptance of the Terms of Use.