*For the most recent entries see the
Petri Nets Newsletter.*

## Automated Performance and Dependability Evaluation Using Model Checking.

Baier, Christel;
Haverkort, Boudewijn;
Hermanns, Holger;
Katoen, Joost-Pieter
In:
M.C. Calzarossa, S. Tucci (Eds.): *Performance Evaluation of Complex Systems: Techniques and Tools*, pages 1-261pp.
Springer Verlag, LNCS 2459,
September 2002.

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.

*Do you need a refined search? Try our search engine
which allows complex field-based queries.*
*Back to the Petri Nets Bibliography*