Skip to Main content Skip to Navigation
New interface
Journal articles

PRISM: probabilistic model checking for performance and reliability analysis

Abstract : Probabilistic model checking is a formal verification technique for the modelling and analysis of stochastic systems. It has proved to be useful for studying a wide range of quantitative properties of models taken from many diffierent application domains. This includes, for example, performance and reliability properties of computer and communication systems. In this paper, we give an overview of the probabilistic model checking tool PRISM, focusing in particular on its support for continuous-time Markov chains and Markov reward models, and how these can be used to analyse performability properties.
Document type :
Journal articles
Complete list of metadata

Cited literature [16 references]  Display  Hide  Download
Contributor : Brigitte Briot Connect in order to contact the contributor
Submitted on : Thursday, February 18, 2010 - 4:38:14 PM
Last modification on : Tuesday, September 8, 2020 - 4:58:02 PM
Long-term archiving on: : Thursday, October 18, 2012 - 3:30:31 PM


Files produced by the author(s)




Marta Kwiatkowska, Gethin Norman, David Parker. PRISM: probabilistic model checking for performance and reliability analysis. ACM SIGMETRICS Performance Evaluation Review, 2009, 36 (4), pp.40-45. ⟨10.1145/1530873.1530882⟩. ⟨inria-00457906⟩



Record views


Files downloads