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

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

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

and

FireWire IEEE 1394 is an interface standard for a serial bus for high-speed communications and isochronous real-time data transfer. It was developed in the late 1980s and early 1990s by Apple in cooperation with a number of companies, primarily Sony a ...

, 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 (people), demonstration, a Sport, sports event, or during looting (this is known as an acting crowd), or ...

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 Biochemistry or biological chemistry is the study of chemical processes within and relating to living organisms. A sub-discipline of both chemistry and biology, biochemistry may be divided into three fields: structural biology, enzymology ...

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 In automata theory, a timed automaton is a finite automaton extended with a finite set of real-valued clocks. During a run of a timed automaton, clock values increase all with the same speed. Along the transitions of the automaton, clock values can ...

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 The University of Oxford is a collegiate research university in Oxford, England. There is evidence of teaching as early as 1096, making it the oldest university in the English-speaking world and the world's second-oldest university in contin ...

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

, 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 user In product development, an end user (sometimes end-user) is a person who ultimately uses or is intended to ulti ...

. 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