AIMS-QuantVer'17: Quantitative verification, part of the Systems Verification course of the AIMS CDT
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.3),
but any version from 4.1 onwards should be fine.
This lab session is self-contained, but if you want information about running PRISM
the best source is the online manual.
There are three parts, of which Parts A and B are of standard difficulty, and Part C is considered advanced:
- 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 an example of a mail delivering robot
and illustrates how to build PRISM models comprising several interacting components.
It uses both DTMCs and Markov decision processes (MDPs).
- Part C
is based on a dynamic power management system,
and illustrates how to build PRISM models comprising multiple interacting components.
It uses both DTMCs and 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.
