PRISM (model checker)
Encyclopedia
PRISM is a probabilistic model checker
, a formal verification
software tool for the modelling and analysis of systems that exhibit probabilistic behaviour . One source of such systems is the use of randomization, for example in communication protocols like Bluetooth
and FireWire, or in security protocols such as Crowds
and Onion routing
. 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 was initially developed at the University of Birmingham
and is now based at the Oxford University Computing Laboratory. It is open-source software
, released under the GNU General Public License
.
Model checking
In computer science, model checking refers to the following problem:Given a model of a system, test automatically whether this model meets a given specification....
, a formal verification
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 methods of mathematics .- Usage :Formal verification can be...
software tool for the modelling and analysis of systems that exhibit probabilistic behaviour . One source of such systems is the use of randomization, for example in communication protocols like Bluetooth
Bluetooth
Bluetooth is a proprietary open wireless technology standard for exchanging data over short distances from fixed and mobile devices, creating personal area networks with high levels of security...
and FireWire, or in security protocols such as Crowds
Crowds
Crowds is a proposed anonymity network that gives probable innocence in the face of a large number of attackers. Crowds was designed by Michael K. Reiter and Aviel D. Rubin and defends against internal attackers and a corrupt receiver, but provides no anonymity against a global attacker or a local...
and Onion routing
Onion routing
Onion routing is a technique for anonymous communication over a computer network. Messages are repeatedly encrypted and then sent through several network nodes called onion routers. Like someone unpeeling an onion, each onion router removes a layer of encryption to uncover routing instructions, and...
. 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 was initially developed at the University of Birmingham
University of Birmingham
The University of Birmingham is a British Redbrick university located in the city of Birmingham, England. It received its royal charter in 1900 as a successor to Birmingham Medical School and Mason Science College . Birmingham was the first Redbrick university to gain a charter and thus...
and is now based at the Oxford University Computing Laboratory. It is open-source software
Open-source software
Open-source software is computer software that is available in source code form: the source code and certain other rights normally reserved for copyright holders are provided under a software license that permits users to study, change, improve and at times also to distribute the software.Open...
, released under the GNU General Public License
GNU General Public License
The GNU General Public License is the most widely used free software license, originally written by Richard Stallman for the GNU Project....
.