Automated Analysis of AODV using UPPAAL

This paper describes an automated, formal and rigorous analysis of the Ad hoc On-Demand Distance Vector (AODV) routing protocol, a popular protocol used in wireless mesh networks. We give a brief overview of a model of AODV implemented in the UPPAAL model checker. It is derived from a process-algebr...

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:
Automation
Diagnostic software
Diagnostic systems
Finite element method
Network topologies
Wireless networks
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:This paper describes an automated, formal and rigorous analysis of the Ad hoc On-Demand Distance Vector (AODV) routing protocol, a popular protocol used in wireless mesh networks. We give a brief overview of a model of AODV implemented in the UPPAAL model checker. It is derived from a process-algebraic model which reflects precisely the intention of AODV and accurately captures the protocol specification. Furthermore, we describe experiments carried out to explore AODV's behaviour in all network topologies up to 5 nodes. We were able to automatically locate problematic and undesirable behaviours. This is in particular useful to discover protocol limitations and to develop improved variants. This use of model checking as a diagnostic tool complements other formal-methods-based protocol modelling and verification techniques, such as process algebra.
ISSN:2331-8422
DOI:10.48550/arxiv.1512.07352