Modelling and Analysis of AODV in 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


2011-10-17


Conference Material


1st International Workshop on Rigorous Protocol Engineering


Vancouver


1-6


This paper describes work in progress towards an automated formal and rigorous analysis of the Ad hoc On-Demand Distance Vector (AODV) routing protocol, a popular protocol used in ad hoc wireless networks. We give a brief overview of a model implemented in the UPPAAL model checker, and describe experiments carried out to explore AODV's behaviour in two network topologies. We were able to locate automatically and confirm some known problematic and undesirable behaviours. We believe this use of model checking as a diagnostic tool complements other formal methods based protocol modelling and verification techniques, such as process algebras. These methods are in particular useful for the discovery of protocol limitations and the development of improved variations.


NICTA


http://wripe11.cis.upenn.edu/


© 2011


English


nicta:5069


Fehnker, Ansgar; van Glabbeek, Robert; Höfner, Peter; McIver, Annabelle; Portmann, Marius; Tan, Wee Lum. Modelling and Analysis of AODV in UPPAAL. In: 1st International Workshop on Rigorous Protocol Engineering; Vancouver. 2011-10-17. 1-6.



Loading citation data...

Citation counts
(Requires subscription to view)