Subscribe
Issue No.05  September/October (2009 vol.35)
pp: 703719
Enrico Vicario , Università di Firenze, Firenze
Luigi Sassoli , Università di Firenze, Firenze
Laura Carnevali , Università di Firenze, Firenze
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TSE.2009.36
ABSTRACT
In the verification of reactive systems with nondeterministic densely valued temporal parameters, the statespace 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 densityfunction which provides a measure for the probability of individual states. To this end, we extend Time Petri Nets by associating a probability densityfunction 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 steadystate 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, nonMarkovian Stochastic Petri Nets, densetime statespace analysis, Difference Bounds Matrix, Markov Renewal Theory.
CITATION
Enrico Vicario, Luigi Sassoli, Laura Carnevali, "Using Stochastic State Classes in Quantitative Evaluation of DenseTime Reactive Systems", IEEE Transactions on Software Engineering, vol.35, no. 5, pp. 703719, September/October 2009, doi:10.1109/TSE.2009.36
REFERENCES
