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.

Using Stochastic State Classes in Quantitative Evaluation of Dense-Time Reactive Systems / E. Vicario; L. Sassoli; L. Carnevali. - In: IEEE TRANSACTIONS ON SOFTWARE ENGINEERING. - ISSN 0098-5589. - STAMPA. - 35:(2009), pp. 703-719. [10.1109/TSE.2009.36]

Using Stochastic State Classes in Quantitative Evaluation of Dense-Time Reactive Systems

VICARIO, ENRICO;CARNEVALI, LAURA
2009

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.
2009
35
703
719
E. Vicario; L. Sassoli; L. Carnevali
File in questo prodotto:
File Dimensione Formato  
TSE09-2.pdf

Accesso chiuso

Tipologia: Versione finale referata (Postprint, Accepted manuscript)
Licenza: Tutti i diritti riservati
Dimensione 2.76 MB
Formato Adobe PDF
2.76 MB Adobe PDF   Richiedi una copia

I documenti in FLORE sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificatore per citare o creare un link a questa risorsa: https://hdl.handle.net/2158/388671
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 66
  • ???jsp.display-item.citation.isi??? 41
social impact