Automated analysis of AODV using UPPAAL

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

doi:10.1007/978-3-642-28756-5_13

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 proceeding › Conference contribution › Academic › peer-review

52 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 language	English
Title of host publication	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
Pages	173-187
Number of pages	15
DOIs	https://doi.org/10.1007/978-3-642-28756-5_13
Publication status	Published - 2012
Externally published	Yes
Event	18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2012 - Tallinn, Estonia Duration: 24 Mar 2012 → 1 Apr 2012 Conference number: 18

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	7214 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2012
Abbreviated title	TACAS 2012
Country/Territory	Estonia
City	Tallinn
Period	24/03/12 → 1/04/12
Other	Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012

Access to Document

10.1007/978-3-642-28756-5_13

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 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 (pp. 173-187). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7214 LNCS). https://doi.org/10.1007/978-3-642-28756-5_13

Fehnker, Ansgar ; Van Glabbeek, Rob ; Höfner, Peter et al. / Automated analysis of AODV using UPPAAL. 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. 2012. pp. 173-187 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{4e3059c4b30d42428bdc8ca46c2315e1,

title = "Automated analysis of AODV using UPPAAL",

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

author = "Ansgar Fehnker and {Van Glabbeek}, Rob and Peter H{\"o}fner and Annabelle McIver and Marius Portmann and Tan, {Wee Lum}",

year = "2012",

doi = "10.1007/978-3-642-28756-5_13",

language = "English",

isbn = "9783642287558",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "173--187",

booktitle = "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",

note = "18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2012, TACAS 2012 ; Conference date: 24-03-2012 Through 01-04-2012",

}

Fehnker, A, Van Glabbeek, R, Höfner, P, McIver, A, Portmann, M & Tan, WL 2012, Automated analysis of AODV using UPPAAL. in 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. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 7214 LNCS, pp. 173-187, 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2012, Tallinn, Estonia, 24/03/12. https://doi.org/10.1007/978-3-642-28756-5_13

Automated analysis of AODV using UPPAAL. / Fehnker, Ansgar; Van Glabbeek, Rob; Höfner, Peter et al.
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. 2012. p. 173-187 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7214 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Automated analysis of AODV using UPPAAL

AU - Fehnker, Ansgar

AU - Van Glabbeek, Rob

AU - Höfner, Peter

AU - McIver, Annabelle

AU - Portmann, Marius

AU - Tan, Wee Lum

N1 - Conference code: 18

PY - 2012

Y1 - 2012

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

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

UR - http://www.scopus.com/inward/record.url?scp=84859363035&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-28756-5_13

DO - 10.1007/978-3-642-28756-5_13

M3 - Conference contribution

AN - SCOPUS:84859363035

SN - 9783642287558

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 173

EP - 187

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

T2 - 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2012

Y2 - 24 March 2012 through 1 April 2012

ER -

Fehnker A, Van Glabbeek R, Höfner P, McIver A, Portmann M, Tan WL. Automated analysis of AODV using UPPAAL. In 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. 2012. p. 173-187. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-28756-5_13

Automated analysis of AODV using UPPAAL

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this