Modelling and Analysis of AODV in UPPAAL

Ansgar Fehnker, Rob J. van Glabbeek, Peter Höfner, Annabelle McIver, Marius Portmann, Wee Lum Tan

Research output: Contribution to conferencePaperAcademic

Abstract

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.
Original languageEnglish
Number of pages6
Publication statusPublished - 23 Dec 2015
Externally publishedYes
Event1st International Workshop on Rigorous Protocol Engineering, WRiPE 2011 - Fairmont Hotel, Vancouver, BC, Canada
Duration: 17 Oct 201117 Oct 2011
Conference number: 1

Conference

Conference1st International Workshop on Rigorous Protocol Engineering, WRiPE 2011
Abbreviated titleWRiPE
CountryCanada
CityVancouver, BC
Period17/10/1117/10/11

Fingerprint

Model checking
Network protocols
Formal methods
Wireless ad hoc networks
Routing protocols
Algebra
Topology
Experiments

Cite this

Fehnker, A., Glabbeek, R. J. V., Höfner, P., McIver, A., Portmann, M., & Tan, W. L. (2015). Modelling and Analysis of AODV in UPPAAL. Paper presented at 1st International Workshop on Rigorous Protocol Engineering, WRiPE 2011, Vancouver, BC, Canada.
Fehnker, Ansgar ; Glabbeek, Rob J. van ; Höfner, Peter ; McIver, Annabelle ; Portmann, Marius ; Tan, Wee Lum. / Modelling and Analysis of AODV in UPPAAL. Paper presented at 1st International Workshop on Rigorous Protocol Engineering, WRiPE 2011, Vancouver, BC, Canada.6 p.
@conference{be9f728e198b4d1db4a37bb627779651,
title = "Modelling and Analysis of AODV in UPPAAL",
abstract = "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.",
author = "Ansgar Fehnker and Glabbeek, {Rob J. van} and Peter H{\"o}fner and Annabelle McIver and Marius Portmann and Tan, {Wee Lum}",
year = "2015",
month = "12",
day = "23",
language = "English",
note = "1st International Workshop on Rigorous Protocol Engineering, WRiPE 2011, WRiPE ; Conference date: 17-10-2011 Through 17-10-2011",

}

Fehnker, A, Glabbeek, RJV, Höfner, P, McIver, A, Portmann, M & Tan, WL 2015, 'Modelling and Analysis of AODV in UPPAAL' Paper presented at 1st International Workshop on Rigorous Protocol Engineering, WRiPE 2011, Vancouver, BC, Canada, 17/10/11 - 17/10/11, .

Modelling and Analysis of AODV in UPPAAL. / Fehnker, Ansgar ; Glabbeek, Rob J. van; Höfner, Peter; McIver, Annabelle; Portmann, Marius; Tan, Wee Lum.

2015. Paper presented at 1st International Workshop on Rigorous Protocol Engineering, WRiPE 2011, Vancouver, BC, Canada.

Research output: Contribution to conferencePaperAcademic

TY - CONF

T1 - Modelling and Analysis of AODV in UPPAAL

AU - Fehnker, Ansgar

AU - Glabbeek, Rob J. van

AU - Höfner, Peter

AU - McIver, Annabelle

AU - Portmann, Marius

AU - Tan, Wee Lum

PY - 2015/12/23

Y1 - 2015/12/23

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

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

M3 - Paper

ER -

Fehnker A, Glabbeek RJV, Höfner P, McIver A, Portmann M, Tan WL. Modelling and Analysis of AODV in UPPAAL. 2015. Paper presented at 1st International Workshop on Rigorous Protocol Engineering, WRiPE 2011, Vancouver, BC, Canada.