Trustworthy Systems

Model Checking Protocols

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

  • Ansgar Fehnker
  • Maryam Kamali

Publications

2015

Abstract PDF Peter Hoefner
Using process algebra to design better protocols (abstract)
Forum “Math-for-Industry” 2015, pp. 31–33, Fukuoka, Japan, October, 2015
Abstract PDF 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

Abstract PDF Ansgar Fehnker, Peter Hoefner, Maryam Kamali and Vinay Mehta
Topology-based mobility models for wireless networks
International Conference on Quantitative Evaluation of SysTems, pp. 16, Buenos Aires, Argentina, August, 2013
Abstract PDF Peter Hoefner and Maryam Kamali
Quantitative analysis of AODV and its variants on dynamic topologies using statistical model checking
International Conference on Formal Modeling and Analysis of Timed Systems, pp. 15, Buenos Aires, Argentina, August, 2013
Abstract PDF 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

Abstract PDF 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
Abstract PDF Ansgar Fehnker, Rob van Glabbeek, Peter Hoefner, Annabelle McIver, Marius Portmann and Wee Lum Tan
Automated analysis of AODV using UPPAAL
International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 173–187, Tallinn, Estonia, March, 2012

2011

Abstract PDF 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

Abstract PDF Mojgan Kamali
Modeling and Verifying the OLSR Protocol Using Uppaal
Information and Communication Technology, Universitetet I Agder, Norway, August, 2014