Paper Info
Title
Quantitative Analysis With the Probabilistic Model Checker PRISM
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.
Year
DOI
Venue
2006
10.1016/j.entcs.2005.10.030
Electr. Notes Theor. Comput. Sci.
Keywords
Field
DocType
probabilistic model,temporal logic,markov model,system modeling,quantitative analysis,dependability,specification language,markov models,numerical method,formal verification,reliability,formal specification,mathematical model
Dependability,Computer science,Correctness,Algorithm,Formal specification,Theoretical computer science,Statistical model,Probabilistic logic,Temporal logic,System model,Formal verification
Journal
Volume
Issue
ISSN
153
2
1571-0661
Citations 
PageRank 
References 
47
1.90
40
Authors
3
Name
Order
Citations
PageRank
Marta Z. Kwiatkowska16118322.21
Gethin Norman24163193.68
David Parker34018184.00