Automated Analysis of AODV using UPPAAL

Select |




Print


Fehnker, Ansgar; van Glabbeek, Robert; Höfner, Peter; McIver, Annabelle; Portmann, Marius; Tan, Wee Lum

Fehnker, Ansgar; van Glabbeek, Robert; Höfner, Peter; McIver, Annabelle; Portmann, Marius; Tan, Wee Lum


2012-03-26


Conference Material


18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012)


Tallinn, Estonia


173-187


This paper describes an automated, formal and rigorous analysis of the Ad hoc On-Demand Distance Vector (AODV) routing protocol, a popular protocol used in wireless mesh networks. We give a brief overview of a model of AODV implemented in the UPPAAL model checker. It is derived from a process-algebraic model which reflects precisely the intention of AODV and accurately captures the protocol specification. Furthermore, we describe experiments carried out to explore AODV's behaviour in all network topologies up to 5 nodes. We were able to automatically locate problematic and undesirable behaviours. This is in particular useful to discover protocol limitations and to develop improved variants. This use of model checking as a diagnostic tool complements other formal-methods-based protocol modelling and verification techniques, such as process algebra.


Springer


Wireless Mesh Networks, routing protocols, model checking, UPPAAL, process algebra


http://www.etaps.org/2012/tacas


0302-9743


nicta:5382


Fehnker, Ansgar; van Glabbeek, Robert; Höfner, Peter; McIver, Annabelle; Portmann, Marius; Tan, Wee Lum. Automated Analysis of AODV using UPPAAL. In: Cormac Flanagan and Barbara König Editor, editor/s. 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012); Tallinn, Estonia. Springer; 2012-03-26. 173-187.



Loading citation data...

Citation counts
(Requires subscription to view)