|
| EPSRC Reference: |
GR/S11107/01 |
| Title: |
Automated Verification of Probabilistic Protocols with Prism |
| Principal Investigator: |
Professor MZ Kwiatkowska |
| Other Investigators: |
|
| Researcher Co-investigator: |
|
| Project Partner: |
|
| Department: |
School of Computer Science |
| Organisation: |
University of Birmingham |
| Scheme: |
Standard Research |
| Starts: |
01 April 2003 |
Ends: |
30 June 2006 |
Value (£): |
181,509
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
Software Engineering |
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary |
|
Probabilistic protocols employ a random element, such as a random number generator or a stream of random bits, in order to arrive at simple, ele and fast algorithmic solutions to a variety of distributed coordination problems. Randomization has proved very effective and is now being used it world situations such as leader election (IEEE 1394 FireWire), Byzantine agreement, multicast protocols and anonymity protocols. A necessary consequence of the inclusion of randomness is the increase in complexity of reasoning about correctness of such algorithms. This proposal build our previous EPSRC-funded research which aimed to develop the foundations and software technology to support automatic verification of probabilistic protocols. PRISM, Probabilistic Symbolic Model Checker, available freely for academic use from URL www.cs.bham.ac.uk/-dxp/prism/, was the outcome of this research. PRISM has already been used to analyse a number of protocols, exposing previously unknown behaviour. However, although PRISM can efficiently handle realistically sized systems, the technology that underpins probabilistic verification still lags well behind the r advances made by conventional model checking: only finite and static configurations can be model checked with PRISM, with no support for abstraction and assume-guarantee reasoning. This proposal aims to address these limitations, and also to further develop the functionality of the tool based c feedback from its users. These will include enhancement with cost/reward functions and a distributed numerical engine.
|
| Final Report Summary |
The aims of this project were to build upon existing EPSRC-funded work on the development of both theoretical foundations and software technology for automatic formal verification of probabilistic systems. In particular, the objectives were to extend and improve the software tool PRISM (www.cs.bham.ac.uk/~dxp/prism/), currently the leading tool in this field, increasing its applicability to larger and more realistic systems.
A range of new probabilistic verification techniques have been successfully devised, implemented and studied throughout the project. These have included symmetry reduction, game-based abstraction, partial order reduction, and methods for model checking of real-time probabilistic systems. For example, symmetry reduction has made it possible to obtain a near factorial state space reduction, and consequently orders-of-magnitude reduction in solution time. Abstraction has been achieved through reduction to 2-player stochastic games, and has resulted in algorithms for approximating the minimum and maximum probability with an interval. Other key advances with respect to the efficiency of PRISM have included the development of parallel and distributed numerical solution algorithms and improvements to underlying symbolic (binary decision diagram based) data structures and algorithms. New formalisms for modelling dynamic environments with probabilistic behaviour, such as mobile wireless networks, have also been developed.
In order to support both the research relating to PRISM and users of the tool, many other enhancements have been made. These include a discrete-event simulation engine as well as improvements to the modelling and property specification languages, user interface and connections to external tools.
The success of the work carried out and of the tool itself can be judged by the increasingly large array of case studies to which PRISM has successfully been applied. These include real-life communication protocols such as Bluetooth and Zeroconf, security protocols for anonymity or contract signing, and many more.
PRISM has been downloaded 4000 times and is widely used for teaching and research at over 30 institutions worldwide. A PRISM page is also maintained at the SourceForge website and there is an active user forum. The bibliography includes 50 external and 70 internal papers related to the theory and usage of PRISM, from a very broad range of application domains: communication protocols, security, distributed computing, performability, dependability, reliability, nanotechnology, and biological processes. Over 40 case studies have been performed, with the PRISM website providing full access to the models and statistics.
|
| Further Information: |
|
| Organisation Website: |
http://www.bham.ac.uk |
|
|