Modelling and Analysis of AODV in UPPAAL

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

Research output: Contribution to conferencePaperpeer-review

Abstract / Description of output

This paper describes work in progress towards an automated formal and rigorous analysis of the Ad hoc OnDemand Distance Vector (AODV) routing protocol, a popular protocol used in ad hoc wireless networks. We give a brief overview of a model of AODV 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. Model checking is in particular useful for the discovery of protocol limitations and in the development of improved variations
Original languageEnglish
Number of pages6
Publication statusPublished - 11 Oct 2011
Event1st International Workshop on Rigorous Protocol Engineering, 2011 - Vancouver, Canada
Duration: 17 Oct 201117 Oct 2011
Conference number: 1


Workshop1st International Workshop on Rigorous Protocol Engineering, 2011
Abbreviated titleWRiPE 2011


Dive into the research topics of 'Modelling and Analysis of AODV in UPPAAL'. Together they form a unique fingerprint.

Cite this