Automated analysis of AODV using UPPAAL

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

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contribution

47 Citations (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems - 18th Int. Conf., TACAS 2012, Held as Part of the European Joint Conf. on Theory and Practice of Software, ETAPS 2012, Proceedings
EditorsCormac Flanagan, Barbara König
Place of PublicationHeidelberg, Germany
PublisherSpringer, Springer Nature
Pages173-187
Number of pages15
Volume7214 LNCS
ISBN (Print)9783642287558
DOIs
Publication statusPublished - 2012
Event18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012 - Tallinn, Estonia
Duration: 24 Mar 20121 Apr 2012

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7214 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012
CountryEstonia
CityTallinn
Period24/03/121/04/12

Fingerprint Dive into the research topics of 'Automated analysis of AODV using UPPAAL'. Together they form a unique fingerprint.

  • Cite this

    Fehnker, A., Van Glabbeek, R., Höfner, P., McIver, A., Portmann, M., & Tan, W. L. (2012). Automated analysis of AODV using UPPAAL. In C. Flanagan, & B. König (Eds.), Tools and Algorithms for the Construction and Analysis of Systems - 18th Int. Conf., TACAS 2012, Held as Part of the European Joint Conf. on Theory and Practice of Software, ETAPS 2012, Proceedings (Vol. 7214 LNCS, pp. 173-187). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7214 LNCS). Heidelberg, Germany: Springer, Springer Nature. https://doi.org/10.1007/978-3-642-28756-5_13