#

## 5th International Workshop on

Formal Methods for Industrial Critical Systems

### Berlin, April 3-4, 2000

# Performance and reliability model checking and model construction

Continuous-time Markov chains (CTMCs) are widely used to describe stochastic
phenomena in many diverse areas. They are used to estimate performance and
reliability characteristics of various nature, for instance to quantify
throughputs of manufacturing systems, to locate bottlenecks in communication
systems, or to estimate reliability in aerospace systems. CTMCs are the
underlying semantic model of major high level performance modelling formalisms
such as stochastic Petri nets, stochastic process algebras, and Markovian
queueing networks.

Model checking is a very successful technique to establish correctness of
systems from very similar application domains, usually described in terms of a
nondeterministic finite-state model. One of the major reasons for the success
of model checking tools in practice is the efficient way to cope with the
state-space explosion problem, using symbolic (BDD-based) techniques.

In this talk, I will introduce CTMCs and discuss the use of model checking to
assess performance and reliability properties of CTMCs. With this approach,
properties-of-interest are expressed as formulas of a stochastic extension of
the logic CTL and interpreted over CTMCs. Model checking this logic requires
the solution of linear systems of equations and of systems of Volterra integral
equations. I will outline approximate techniques for solving the equation
systems, and present a JAVA implementation of a Markov chain model checker.

My introduction to CTMC model checking will be complemented with a discussion
of CTMC model construction techniques. I will survey formal methods that
facilitate the construction of large CTMC models. In particular I will focus on
high-level formalisms supporting a modern, hierarchical and compositional
design methodology. Existing tool support, as well as techniques to combat the
state space explosion problem will be discussed.

__Note:__ The content of the following files is part of
GMD Report No. 91
and subject to its copyright.

ERCIM FMICS Home Page,
GMD FOKUS Home Page

Last modified: Wednesday, 19-Apr-2000 08:57:51 MET DST,
Axel Rennoch