Modelling and Analysis of AODV in UPPAAL
line

Ansgar Fehnker1,2, Rob van Glabbeek1,2, Peter Höfner1,2,
Annabelle McIver4,1, Marius Portmann1,3 and Wee Lum Tan1,3
1NICTA, Australia
2University of New South Wales, Australia
3The University of Queensland, Australia
4Macquarie University, Australia

Abstract
line

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 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.

Data
line

In this paper we use the UPPAAL model checker to obtain an executable version of a process algebra formalisation of AODV. Here, we list the input files of the examples presented in our paper.

ExampleInputTopology
AODV does not always establish routes UPPAAL input
AODV can produce non-optimal routes
(Example I)
UPPAAL input
AODV can produce non-optimal routes
(Example II)
UPPAAL input