Modelling and Analysis of AODV in UPPAAL

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

Full description

Saved in:
Bibliographic Details
Published in:arXiv.org 2015-12
Main Authors: Fehnker, Ansgar, Rob van Glabbeek, Höfner, Peter, McIver, Annabelle, Portmann, Marius, Wee Lum Tan
Format: Article
Language:English
Subjects:
Ad hoc networks
Diagnostic software
Diagnostic systems
Modelling
Network topologies
Wireless networks
Workflow
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:2331-8422