David Parker
Reader, Computer Science, University of Birmingham
[KNP05d] Marta Kwiatkowska, Gethin Norman and David Parker. Quantitative Analysis with the Probabilistic Model Checker PRISM. Electronic Notes in Theoretical Computer Science, 153(2), pages 5-31, Elsevier. May 2005. [ps.gz] [pdf] [bib] [Gives an overview of PRISM and describes a selection of case studies.]
Downloads:  ps.gz ps.gz (231 KB)  pdf pdf (508 KB)  bib bib
Notes: ENTCS is available at www.sciencedirect.com/science/journal/15710661.
Abstract. Probabilistic model checking is a formal verification technique for establishing the correctness, performance and reliability of systems which exhibit stochastic behaviour. As in conventional verification, a precise mathematical model of a real-life system is constructed first, and, given formal specifications of one or more properties of this system, an analysis of these properties is performed. The exploration of the system model is exhaustive and involves a combination of graph-theoretic algorithms and numerical methods. In this paper, we give a brief overview of the probabilistic model checker PRISM (www.cs.bham.ac.uk/~dxp/prism) implemented at the University of Birmingham. PRISM supports a range of probabilistic models and specification languages based on temporal logic, and has been recently extended with costs and rewards. We describe our experience with using PRISM to analyse a number of case studies from a wide range of application domains. We demonstrate the usefulness of probabilistic model checking techniques in detecting flaws and unusual trends, focusing mainly on the quantitative analysis of a range of best, worst and average-case system characteristics.