Analyzing Mobile ad hoc Network Protocols via Probabilistic Model Checking

April 26, 2005
Marta Kwiatkowska | University of Birmingham

Ad hoc networks are formed as collections of nodes that communicate over wireless channels. The dynamic and distributed nature of such networks means that randomization is often used to improve efficiency and to achieve symmetric solutions. In this talk, we demonstrate the applicability of an automated formal verification technique called probabilistic model checking to the analysis of ad hoc network protocols. A probabilistic model checker calculates the probability of a given temporal logic property being satisfied, as opposed to validity. Probabilistic specifications typically express statements such as “is leader election eventually resolved with probability 1?”, “what is the expected time to deliver one message?”, and “what is the probability that the message will be delivered within 30ms?”. The usefulness of the techniques will be demonstrated through a number of case studies analyzing real-world protocols performed with PRISM, a probabilistic symbolic model checker developed at the University of Birmingham (www.cs.bham.ac.uk/~dxp/prism/). Examples will include the Zeroconf dynamic configuration protocol for IPv4 link-local addresses and Bluetooth device discovery.

Speaker Details

Marta Kwiatkowska is Professor of Computer Science in the School of Computer Science at the University of Birmingham, and Director of the Midlands e-Science Centre of Excellence in Modelling and Analysis of Large Complex Systems. She has internationally leading expertise in probabilistic modelling and verification, and was invited speaker at the 18th Logic in Computer Science Symposium (LICS03). Kwiatkowska led the development of state-of-the-art probabilistic model checking software tool PRISM (www.cs.bham.ac.uk/~dxp/prism/), a research programme funded by EPSRC, DTI and QinetiQ. PRISM has been used worldwide to analyse a range of communication protocols, including Bluetooth device discovery, dynamic power management, nanotechnology designs, randomized distributed algorithms and metabolic pathways. Kwiatkowska’s current research projects concern probabilistic model checking, verification of asynchronous hardware, ubiquitous computing, ad hoc network protocols, modeling of biological processes, e-Science and grid computing. She recently co-authored a book, Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems, AMS 2004 (www.cs.bham.ac.uk/~dxp/publications/KNP04a.html). Kwiatkowska is editor of Transactions on Computational Systems Biology and Journal of Logical Methods in Computer Science (LMCS), regularly serves on conference programme committees and is involved in the UK Grand Challenges initiative on Ubiquitous Computing. For more details see www.cs.bham.ac.uk/~mzk.