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...

• Type: Conference
• Year: 2002
• Where: DSN
• Authors: Boudewijn R. Haverkort, Lucia Cloth, Holger Hermanns, Joost-Pieter Katoen, Christel Baier
• Keywords: Computational Procedures, Computer Networks, DSN 2002, Markov Reward Models, Model Checking