Probability features increasingly often in communication protocols: it is used in distributed co-ordination as a symmetry breaker, in exponential backoff, and to provide adaptive resource management strategies. In this talk, we demonstrate the applicability of an automated formal verification technique called probabilistic model checking to protocol analysis. 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 analysing real-world protocols performed with PRISM, a probabilistic symbolic model checker developed at the University of Birmingham. Examples will include Bluetooth device discovery, Zigbee and the Zeroconf dynamic configuration protocol for IPv4 link-local addresses. The talk will also give an overview of recent developments in probabilistic model checking, including sampling based methods and model reduction techniques.
| Prof. Marta Kwiatkowska |
| University of Birmingham |
| Date: | Thu Apr 20 2006 |
| Time: | 11 to 12pm |
| Location: | Level 1 Seminar Room, 223 Anzac Parade, Kensington |
| Convened by: | Ron van der Meyden |
Last updated by tbourke at Fri Apr 7 15:29:08 2006 GMT+1000