Model Checking Performability Properties

10 years 6 months ago
Model Checking Performability Properties
Model checking has been introduced as an automated technique to verify whether functional properties, expressed in a formal logic like computational tree logic (CTL), do hold in a formally-specified system. In recent years, we have extended CTL such that it allows for the specification of properties over finite-state continuous-time Markov chains (CTMCs). Computational techniques for model checking have been developed and successfully applied in the dependability context. Further work in this area has recently led to the continuous stochastic reward logic (CSRL), a logic to specify measures over CTMCs extended with a reward structure (socalled Markov reward models). Well-known performability measures, most notably also Meyer’s performability distribution, can be easily defined with CSRL. However, using CSRL it is possible to specify performability measures that have not yet been addressed in the literature, hence, for which no computational procedures have been developed yet. In...
Boudewijn R. Haverkort, Lucia Cloth, Holger Herman
Added 14 Jul 2010
Updated 14 Jul 2010
Type Conference
Year 2002
Where DSN
Authors Boudewijn R. Haverkort, Lucia Cloth, Holger Hermanns, Joost-Pieter Katoen, Christel Baier
Comments (0)