David Parker
Reader, Computer Science, University of Birmingham
[KNP05b] Marta Kwiatkowska, Gethin Norman and David Parker. Probabilistic Model Checking in Practice: Case Studies with PRISM. ACM SIGMETRICS Performance Evaluation Review, 32(4), pages 16-21. March 2005. [ps.gz] [pdf] [bib] [Surveys a selection of case studies that have been carried out using PRISM.]
Downloads:  ps.gz ps.gz (41 KB)  pdf pdf (100 KB)  bib bib
Abstract. In this paper, we describe some practical applications of probabilistic model checking, a technique for the formal analysis of systems which exhibit stochastic behaviour. We give an overview of a selection of case studies carried out using the probabilistic model checking tool PRISM, demonstrating the wide range of application domains to which these methods are applicable. We also illustrate several benefits of using formal verification techniques to analyse probabilistic systems, including: (i) that they allow a wide range of numerical properties to be computed accurately; and (ii) that they perform a complete and exhaustive analysis enabling, for example, a study of best- and worst-case scenarios.