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 (statespace 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.
 OnGoing 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

 Ansgar Fehnker
 Maryam Kamali

Publications
2015


Peter Hoefner
Using process algebra to design better protocols (abstract)
Forum “MathforIndustry” 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
Topologybased 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 
Contact
Peter Höfner, peter.hoefner <at> data61.csiro.au