Funded by:
(grant reference GR/S11107/01)
(and also QinetiQ)
Dates: 2003-2006
| Institutions: |  | University of Birmingham |
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.