www.prismmodelchecker.org

PRISM Tutorial

This tutorial will introduce you to the PRISM tool using a selection of example models.

The tutorial comprises several parts. You should complete part 1 first. After that, you should be able to look at the remaining parts in any order. If anything is unclear, the best place to look for answers is the PRISM manual.

  • Part 1: This 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 2: This uses another simple randomised algorithm - Herman's self-stabilisation algorithm, which is also modelled as a DTMC. It introduces some additional features of the PRISM modelling and property languages.

  • Part 3: This introduces a continuous-time Markov chain (CTMC) example and is based on an analysis of dynamic power management systems in PRISM.

  • Part 4: This demonstrates the use of PRISM to study a biological case study, a circadian clock, modelled as a CTMC.

  • Part 5: This uses a case study from the field of security, the EGL contract signing protocol, modelled as a DTMC.

  • Part 6: This introduces a Markov decision process (MDP) example: the dining philosphers problem.

If you have questions, comments, or suggestions regarding this tutorial, please contact us.










Documentation