Issue No. 05 - September/October (2009 vol. 35)

ISSN: 0098-5589

pp: 703-719

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

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. , pp. 703-719, September/October 2009, doi:10.1109/TSE.2009.36