Oxford logo

Automated Verification of Probabilistic Protocols with PRISM

Project details

Funded by: EPSRC (grant reference GR/S11107/01) (and also QinetiQ)

Dates: 2003-2006

Institutions: University of Birmingham

Abstract

Probabilistic protocols employ a random element, such as a random number generator or a stream of random bits, in order to arrive at simple, elegant and fast algorithmic solutions to a variety of distributed coordination problems. Randomization has proved very effective and is now being used in real-world situations such as leader election (IEEE 1394 FireWire), Byzantine agreement, multicast protocols (Spinglass project) and anonymity protocols (Crowds). A necessary consequence of the inclusion of randomness is the increase in complexity of reasoning about correctness of such algorithms, which must combine probabilistic analysis with conventional reasoning, and thus calls for automated verification methods and tools. This proposal builds on our previous EPSRC-funded research which aimed to develop the foundations and software technology to support such verification. PRISM, Probabilistic Symbolic Model Checker, which is freely available, was the outcome of this research. PRISM has already been used to verify several probabilistic protocols including FireWire root contention. However, although PRISM can efficiently handle realistically sized systems, the technology that underpins probabilistic verification still lags well behind the recent advances made by conventional model checking: only finite and static configurations can be model checked with PRISM, with no support for abstraction and proof techniques. This proposal aims to address these limitations, and also to further develop the functionality of the tool based on feedback from its users.

Aims

  • Guided by case studies, to enhance the modelling capability of the probabilistic model checker PRISM and the expressiveness of its specification languages.
  • To formulate appropriate notions of data type reduction for probabilistic systems and implement them within the tool.
  • To develop foundations of verification methodology for probabilistic systems and, if successful, build a prototype proof assistant layer over PRISM.
  • To formulate an appropriate model for representing dynamically changing distributed probabilistic environments and investigate model checking methods for those.

People

Further information

QAV:

Home

People

Projects

Publications