PRISM is a probabilistic

model checker In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification (also known as correctness). This is typically associated with hardware or software system ...

, a

formal verification In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal met ...

software tool for the modelling and analysis of systems that exhibit probabilistic behaviour.Kwiatkowska, M.; Norman, G.; Parker, D. "Probabilistic model checking in practice: Case studies with PRISM". ''ACM SIGMETRICS Performance Evaluation Review'', 32(4), pages 16–21. One source of such systems is the use of

randomization Randomization is the process of making something random. Randomization is not haphazard; instead, a random process is a sequence of random variables describing a process whose outcomes do not follow a deterministic pattern, but follow an evolution d ...

, for example in communication protocols like

Bluetooth Bluetooth is a short-range wireless technology standard that is used for exchanging data between fixed and mobile devices over short distances and building personal area networks (PANs). In the most widely used mode, transmission power is limi ...

and FireWire, or in security protocols such as

Crowds Generally speaking, a crowd is defined as a group of people that have gathered for a common purpose or intent such as at a demonstration, a sports event, or during looting (this is known as an acting crowd), or may simply be made up of many ...

and

Onion routing Onion routing is a technique for anonymous communication over a computer network. In an onion network, messages are encapsulated in layers of encryption, analogous to layers of an onion. The encrypted data is transmitted through a series of net ...

. Stochastic behaviour also arises in many other computer systems, for example due to equipment failures or unpredictable communication delays. Yet another class of systems amenable to this kind of analysis are biochemical reaction networks. PRISM can be used to analyse several different types of probabilistic models, including discrete-time Markov chains, continuous-time Markov chains, Markov decision processes and probabilistic extensions of the timed automata formalism. Properties to be verified against these models are expressed in probabilistic extensions of

temporal logic In logic, temporal logic is any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time (for example, "I am ''always'' hungry", "I will ''eventually'' be hungry", or "I will be hungry ''until'' I ...

. Development of PRISM is primarily carried out at the

University of Birmingham The University of Birmingham (informally Birmingham University) is a Public university, public research university located in Edgbaston, Birmingham, United Kingdom. It received its royal charter in 1900 as a successor to Queen's College, Birmingha ...

and the

University of Oxford , mottoeng = The Lord is my light , established = , endowment = £6.1 billion (including colleges) (2019) , budget = £2.145 billion (2019–20) , chancellor ...

. The tool is

open-source software Open-source software (OSS) is computer software that is released under a license in which the copyright holder grants users the rights to use, study, change, and distribute the software and its source code to anyone and for any purpose. Op ...

, released under the

GNU General Public License The GNU General Public License (GNU GPL or simply GPL) is a series of widely used free software licenses that guarantee end users the four freedoms to run, study, share, and modify the software. The license was the first copyleft for general ...

. PRISM has been selected for the

Google Summer of Code The Google Summer of Code, often abbreviated to GSoC, is an international annual program in which Google awards stipends to contributors who successfully complete a free and open-source software coding project during the summer. , the program is ...

programme in 2013 and 2014.

References

External links

PRISM websitePRISM case studies repository
Model checkers Free application software Probabilistic software {{formalmethods-stub