www.prismmodelchecker.org

SSFT'14: Probabilistic model checking with PRISM

PRISM Lab Session

This hands-on tool session will introduce you to PRISM. To get started, download and install it. It is best to make sure that you are running the latest version (currently 4.2), but any version from 4.1 onwards should be fine.

This tutorial is self-contained, but if you want information about running PRISM, the best source of information is the online manual.

There are two parts:

  • Part A uses a simple discrete-time Markov chain (DTMC) example - a randomised algorithm for modelling a 6-sided die with a fair coin. It introduces the basics of the PRISM modelling language and the PRISM tool.

  • Part B is based on a dynamic power management system, and illustrates how to build PRISM models comprising multiple interacting components. It uses both DTMC and Markov decision processes (MDPs)

If you want to learn about other aspects of PRISM, take a look at the main online tutorial.

You can also find many more interesting examples in the case studies section of the website.

Documentation