  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.
