| EPSRC Reference: |
GR/S11107/01 |
| Title: |
Automated Verification of Probabilistic Protocols with Prism |
| Principal Investigator: |
Kwiatkowska, Professor MZ |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
School of Computer Science |
| Organisation: |
University of Birmingham |
| Scheme: |
Standard Research (Pre-FEC) |
| 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 on Grant Application Form |
|
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.
|
|
Key Findings |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Potential use in non-academic contexts |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Impacts |
|
| Description |
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk |
| Summary |
|
| Date Materialised |
|
|
|
|
Sectors submitted by the Researcher |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
| Project URL: |
|
| Further Information: |
|
| Organisation Website: |
http://www.bham.ac.uk |