PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems which exhibit random or probabilistic behaviour. It supports four types of probabilistic models:

• discrete-time Markov chains (DTMCs)
• continuous-time Markov chains (CTMCs)
• Markov decision processes (MDPs)
• probabilistic timed automata (PTAs)

PRISM has been used to analyse systems from a wide range of application domains, including communication and multimedia protocols, randomised distributed algorithms, security protocols, biological systems and many others. Full details for more than 40 such case studies can be found on the tool website (see below).

Models are described using the PRISM language, a simple, state-based language. PRISM provides support for automated analysis of a wide range of quantitative properties of these models, e.g.: "what is the probability of a failure causing the system to shut down within 4 hours?", "what is the worst-case probability of the protocol terminating in error, over all possible initial configurations?", "what is the expected size of the message queue after 30 minutes?", or "what is the worst-case expected time taken for the algorithm to terminate?". The property specification language incorporates the temporal logics PCTL and CSL, as well as extensions for quantitative specifications and costs/rewards.

PRISM is open source software and is supported on Linux, Windows, Mac OS X and Solaris. Binary versions and source code can be obtained from the tool web site. The site also includes a bibliography of PRISM-related publications, a manual, a tutorial and slides for lecture course.