Title :
Correctness Verification and Quantitative Evaluation of Timed Systems Based on Stochastic State Classes
Author_Institution :
Univ. di Firenze, Florence
Abstract :
This tutorial addresses the integration of correctness verification and quantitative evaluation of timed systems, based on the stochastic extension of the theory of DBM state classes. In the first part, we recall symbolic state space analysis of non-deterministic models based on DBM state classes, describing the algorithms for state space enumeration and for timing analysis of individual traces.
Keywords :
Markov processes; formal verification; state-space methods; stochastic systems; symbol manipulation; Markov renewal theory; correctness verification; quantitative evaluation; state space enumeration; stochastic state classes; symbolic manipulation; symbolic state space analysis; timed systems; Algorithm design and analysis; Density functional theory; Informatics; Probability density function; Real time systems; Software quality; State-space methods; Stochastic processes; Stochastic systems; Timing;
Conference_Titel :
Quantitative Evaluation of Systems, 2008. QEST '08. Fifth International Conference on
Conference_Location :
St. Malo
Print_ISBN :
978-0-7695-3360-5
DOI :
10.1109/QEST.2008.53
