|
| EPSRC Reference: |
GR/S46727/01 |
| Title: |
Probabilistic Model Checking of Mobile Ad Hoc Network Protocols |
| 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 November 2003 |
Ends: |
31 October 2006 |
Value (£): |
162,803
|
| EPSRC Research Topic Classifications: |
| ICT Networks and Distributed Systems |
|
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary |
|
Ubiquitous computing entails networks of mobile, portable or wearable devices, communicating over wireless medium in a distributed scenario, operating in a timely fashion and at low power. The combination of distributed environment and dynamic topology makes reliability guarantees difficult to achieve, yet dependability assurance is essential before deployment. High failure rate of transmission in the wireless medium and the resulting delays necessitate probabilistic modelling, while the requirement to operate at low power demands dynamic power management policies. Unfortunately, conventional analysis and prediction methods have limitations: simulation is cumbersome and yields coarse estimates that are difficult to reproduce in practice, and analytical approaches fail in a dynamic context. This proposal aims to apply and adapt probabilistic model checking techniques (www.cs.bham.ac.uk/-dxp/prism/) to the modelling and analysis of mobile ad hoc network protocols, in order to develop automated design validation methods capable of performance prediction and correctness assurance. It is a radical new approach that capitalises on the UK leading position and has the potential to deliver a toolset of theoretical results, algorithms, and proof-of-concept implementation, and evaluate it on real-world case studies through academic and industrial collaborations.
|
| Final Report Summary |
The central aim of this project was to develop theoretical foundations for modelling and evaluating mobile ad hoc network protocol designs based on probabilistic model checking techniques. Wireless ad hoc networks are communication networks which connect devices such as PDAs, laptops and other portables in a spontaneous fashion, without a fixed infrastructure such as a backbone LAN. The control of such networks is de-centralised, and the protocols have to deal with a distributed environment, dynamic topology, high failure rate of transmissions and energy limitations. Probabilistic modelling is therefore essential, but conventional analysis methods, such as simulation, are approximate and yield coarse performance predictions. In contrast, probabilistic model checking can obtain exact performance characteristics, and is automatic.
Probabilistic model checking research aims at the foundations, implementation and applications of the techniques to real-world case studies. The probabilistic model checker PRISM (www.cs.bham.ac.uk/~dxp/prism/) developed in Kwiatkowska's group and first relesed in 2001 has established itself as the international leader in the area. This project aimed to extend the application domain of probabilistic model checking to ad hoc network protocols, and appropriately enhance the foundations and software technology for probabilistic model checking as implemented in PRISM.
The research concentrated on developing new modelling formalisms that allow for probabilistic behaviour, real-time aspects, node mobility and dynamic/spatial environments. In the quest for automatic verification of such systems, a range of novel probabilistic verification techniques and methodologies have been successfully devised and implemented throughout the project. These include symbolic methods for model checking of real-time probabilistic systems and systems exhibiting general probability distributions, symmetry reduction, game-based abstraction and partial order reduction. Other key advances have included the development of efficiency improvements to the underlying data structures and algorithms used in PRISM, as well as methods to enhance scalability such as approximate solution.
The applicability of the probabilistic model checking approach has been demonstrated through a number of real-world protocols from the mobile ad hoc network domain, including the device discovery protocol of the wireless communication standard Bluetooth, the collision avoidance mechanism of the IEEE 802.3 standard, the ZeroConf dynamic configuration protocol for IPv4 link-local addresses, the contention resolution protocol of the IEEE 802.11 wireless local area network standard, and dynamic power management schemes.
Since the start of this project, the probabilistic model checking approach has been taken up internationally, and its importance - not only for ad hoc networks, but more generally for ubiquitous computing - has been recognised e.g. through the WINES and the Grand Challenge in Computing initiatives. The benefits of the research are new techniques for calculating exact performance metrics which cannot be obtained with simulation, and consequently improved dependability and performance of networking protocols.
|
| Further Information: |
|
| Organisation Website: |
http://www.bham.ac.uk |
|
|