Model Checking Protocols
-
Aim: use exhaustive and statistical model checking techniques to analyse and verify routing and communication protocols.
- Context: The use of model checking technique for the analysis of protocols is part of Formal Methods for Wireless Networks.
- Approach: To complement our process algebraic approach we use the model checker UPPAAL for an automated, formal and rigorous analysis of wireless mesh network routing protocols. In particular, we obtain executable versions of specifications written in the process algebra AWN, in the language of the UPPAAL model checker. By deriving the UPPAAL model from the AWN model, the accuracy of the AWN model is transferred to the UPPAAL model.
- Collaboration: Macquarie University, University of South Pacific, Turku Centre for Computer Science (TUCS) & Åbo Akademi University
Activities
- Exhaustive Model Checking: The AODV routing protocol has been specified in the process algebra AWN. We show how to obtain executable version of this specification, in the language of the UPPAAL model checker. By deriving the UPPAAL model from the AWN model, the accuracy of the AWN model is transferred to the UPPAAL model.
The executable UPPAAL model is used to confirm and discover the presence of undesirable behaviour. We check important properties against all topologies of up to 5 nodes, which also includes dynamic topologies with one link going up or down.
This exhaustive search confirmed known and revealed new problems of AODV, and let us quantify in how many topologies a particular error can occur.- Statistical Model Checking: Dynamic topology changes, e.g. as a consequence of mobile nodes, and network sizes up to hundreds of nodes often rule out exhaustive model checking for realistic scenarios (state-space explosion). Statistical Model Checking, however, can overcome these problems and, moreover, allows a quantitative analysis. We demonstrate that statistical model checking can be used for formal reasoning of routing protocols in wireless networks.
- On-Going Work: is to fully complement by model checking any protocol specification given in AWN. Having the ability of automatically deriving an UPPAAL model from an AWN specification and thus model checking formal specifications allows the confirmation and detailed diagnostics of suspected errors. The availability of an executable model becomes especially useful in the evaluation of proposed improvements to AODV, as we have shown. We have set up an environment where we can test a whole bunch of different topologies in a systematic manner. This will allow us to do a fast comparison between standard AODV and proposed variations in contexts known to be problematic.
People
|
|
Publications
2015
|
 |
Peter Hoefner Using process algebra to design better protocols (abstract) Forum “Math-for-Industry” 2015, pp. 31–33, Fukuoka, Japan, October, 2015 |
|
|
|
Mojgan Kamali, Peter Hoefner, Maryam Kamali and Luigia Petre Formal analysis of proactive, distributed routing Software Engineering and Formal Methods, pp. 15, York, UK, September, 2015 |
2013
|
|
|
Ansgar Fehnker, Peter Hoefner, Maryam Kamali and Vinay Mehta Topology-based mobility models for wireless networks Proceedings of the 10th International Conference on Quantitative Evaluation of SysTems, pp. 16, Buenos Aires, Argentina, August, 2013 |
|
|
|
Peter Hoefner and Maryam Kamali Quantitative analysis of AODV and its variants on dynamic topologies using statistical model checking 11th International Conference on Formal Modeling and Analysis of Timed Systems, pp. 15, Buenos Aires, Argentina, August, 2013 |
|
|
|
Peter Hoefner and Annabelle McIver Statistical model checking of wireless mesh routing protocols 5th NASA Formal Methods Symposium (NFM 2013), pp. 15, Moffett Field, CA, USA, May, 2013 |
2012
|
|
|
Peter Hoefner and Sarah Edenhofer Towards a rigorous analysis of AODVv2 (DYMO) 2nd International Workshop on Rigorous Protocol Engineering (WRiPE 2012), pp. 1–6, Austin, Texas, October, 2012 |
|
|
|
Ansgar Fehnker, Rob van Glabbeek, Peter Hoefner, Annabelle McIver, Marius Portmann and Wee Lum Tan Automated analysis of AODV using UPPAAL Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 173–187, Tallinn, Estonia, March, 2012 |
2011
|
|
|
Ansgar Fehnker, Rob van Glabbeek, Peter Hoefner, Annabelle McIver, Marius Portmann and Wee Lum Tan Modelling and analysis of AODV in UPPAAL 1st International Workshop on Rigorous Protocol Engineering, pp. 1–6, Vancouver, October, 2011 |
Master's theses
 |
|
Mojgan Kamali Modeling and Verifying the OLSR Protocol Using Uppaal Information and Communication Technology, Universitetet I Agder, Norway, August, 2014 |