Model Checking for Probability and Time: from Theory to Practice
Marta Kwiatkowska*
University of Birmingham
Probability features increasingly often in software and hardware
systems: it is used in distributed co-ordination and routing
problems, to model fault-tolerance and performance, and to provide
adaptive resource management strategies. Probabilistic model
checking is an automatic procedure for establishing if a desired
property holds in a probabilistic model, aimed at verifying
probabilistic specifications such as ``leader election is
eventually resolved with probability 1'', ``the chance of shutdown
occurring is at most 0.01%'', and ``the probability that a
message will be delivered within 30ms is at least 0.75''. A
probabilistic model checker calculates the probability of a
given temporal logic property being satisfied, as opposed to
validity. In contrast to conventional model checkers, which rely
on reachability analysis of the underlying transition system
graph, probabilistic model checking additionally involves
numerical solutions of linear equations and linear programming
problems. This paper reports our experience with implementing
PRISM (www.cs.bham.ac.uk/~dxp/prism/), a Probabilistic
Symbolic Model Checker, demonstrates its usefulness in
analysing real-world probabilistic protocols, and outlines future
challenges for this research direction.
* Marta Kwiatkowska is Professor of Computer Science at the University
of Birmingham where she works with the research group on Modelling and
Analysis of Systems.
