# Automated performance and dependability evaluation using model checking

Baier, Christel
and
Haverkort, Boudewijn
and
Hermanns, Holger
and
Katoen, Joost-Pieter
(2002)
*Automated performance and dependability evaluation using model checking.*
In:
M. Calzarossa
&
S. Tucci
(Eds.),
Computer Performance Evaluation.
Lecture Notes in Computer Science, 2459
.
Springer Verlag, Berlin, pp. 261-289.
ISBN 9783540442523

PDF
Restricted to UT campus only 340kB |

Abstract: | Markov chains (and their extensions with rewards) have been widely used to determine performance, dependability and performability characteristics of computer communication systems, such as throughput, delay, mean time to failure, or the probability to accumulate at least a certain amount of reward in a given time.
Due to the rapidly increasing size and complexity of systems, Markov chains and Markov reward models are difficult and cumbersome to specify by hand at the state-space level. Therefore, various specification formalisms, such as stochastic Petri nets and stochastic process algebras, have been developed to facilitate the specification of these models at a higher level of abstraction. Up till now, however, the specification of the measure-of-interest is often done in an informal and relatively unstructured way. Furthermore, some measures-of-interest can not be expressed conveniently at all. In this tutorial paper, we present a logic-based specification technique to specify performance, dependability and performability measures-of-interest and show how for a given finite Markov chain (or Markov reward model) such measures can be evaluated in a fully automated way. Particular emphasis will be given to so-called path-based measures and hierarchically-specified measures. For this purpose, we extend so-called model checking techniques to reason about discrete- and continuous-time Markov chains and their rewards. We also report on the use of techniques such as (compositional) model reduction and measure-driven state-space generation to combat the infamous state space explosion problem. |

Item Type: | Book Section |

Copyright: | © 2002 Springer |

Faculty: | Electrical Engineering, Mathematics and Computer Science (EEMCS) |

Research Group: | |

Link to this item: | http://purl.utwente.nl/publications/63274 |

Official URL: | http://www.springerlink.com/content/bqk287j30tcu7kpb/ |

Export this item as: | BibTeX EndNote HTML Citation Reference Manager |

Repository Staff Only: item control page