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
- 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.