Probabilistic Model Checking with PRISM

Contact:
Prof Marta Kwiatkowska
School of Computer Science
The University of Birmingham
Edgbaston, Birmingham
B15 2TT, United Kingdom

Email: informatics-crn-enquiries[at]cs.bham.ac.uk
Website: http://www.cs.bham.ac.uk/research/systems/probabilistic/

Computer software is being used in many critical applications, for example flight controllers and network routing, and it is therefore essential that it works as expected. Model checking is an automatic verification approach that inputs a model of the system and a specification, and then explores all system executions in order to check if the specification holds. The challenge is in finding efficient representations of models to make such explorations feasible. Probabilistic model checking concerns verification of probabilistic systems. Randomisation is frequently used in real-world distributed coordination protocols, fault-tolerant algorithms and in adaptive schemes.

At Birmingham, we have implemented PRISM, the internationally leading probabilistic model checker. PRISM enables quantitative analysis of properties such as expected time, average power consumption, and probability of delivery by deadline. It has been used to model and analyse over 30 real-world protocols, which included anonymity protocols for the Internet, Bluetooth device discovery, dynamic power management, nanotechnology designs and biochemical reactions. For example, it was discovered with PRISM that the Crowds anonymity protocol does not in fact guarantee anonymity, and that the worst case time to hear one message during Bluetooth device discovery is 2.5 seconds.

PRISM was also used to analyse the IEEE 1394 FireWire root contention protocol, a randomised leader election protocol which uses an electronic coin. Analysis with PRISM confirmed that a biased coin gives an advantage.