Modelling and analysis of AODV in UPPAAL

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

Modelling and analysis of AODV in UPPAAL

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

School of Computing

Research output: Contribution to conference › Paper › peer-review

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 language	English
Pages	1-6
Number of pages	6
Publication status	Published - 2011
Event	1st International Workshop on Rigorous Protocol Engineering, WRiPE 2011 - Vancouver, Canada Duration: 17 Oct 2011 → 20 Oct 2011

Conference

Conference	1st International Workshop on Rigorous Protocol Engineering, WRiPE 2011
Country/Territory	Canada
City	Vancouver
Period	17/10/11 → 20/10/11

Access to Document

https://web.archive.org/web/20141127040134/http://wripe11.cis.upenn.edu/program/papers/wripe11-paper10.pdf

Cite this

Fehnker, A., van Glabbeek, R., Höfner, P., McIver, A., Portmann, M., & Tan, W. L. (2011). Modelling and analysis of AODV in UPPAAL. 1-6. Paper presented at 1st International Workshop on Rigorous Protocol Engineering, WRiPE 2011, Vancouver, British Columbia, Canada. https://web.archive.org/web/20141127040134/http://wripe11.cis.upenn.edu/program/papers/wripe11-paper10.pdf

@conference{da017d506c744aa981a7c93a724a107f,

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 {van Glabbeek}, Rob and Peter H{\"o}fner and Annabelle McIver and Marius Portmann and Tan, {Wee Lum}",

year = "2011",

language = "English",

pages = "1--6",

note = "1st International Workshop on Rigorous Protocol Engineering, WRiPE 2011 ; Conference date: 17-10-2011 Through 20-10-2011",

}

Fehnker, A, van Glabbeek, R, Höfner, P, McIver, A, Portmann, M & Tan, WL 2011, 'Modelling and analysis of AODV in UPPAAL', Paper presented at 1st International Workshop on Rigorous Protocol Engineering, WRiPE 2011, Vancouver, Canada, 17/10/11 - 20/10/11 pp. 1-6. <https://web.archive.org/web/20141127040134/http://wripe11.cis.upenn.edu/program/papers/wripe11-paper10.pdf>

TY - CONF

T1 - Modelling and analysis of AODV in UPPAAL

AU - Fehnker, Ansgar

AU - van Glabbeek, Rob

AU - Höfner, Peter

AU - McIver, Annabelle

AU - Portmann, Marius

AU - Tan, Wee Lum

PY - 2011

Y1 - 2011

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.

UR - http://www.cs.utah.edu/~mprobst/ICNP2011/index.html

M3 - Paper

SP - 1

EP - 6

T2 - 1st International Workshop on Rigorous Protocol Engineering, WRiPE 2011

Y2 - 17 October 2011 through 20 October 2011

ER -

Modelling and analysis of AODV in UPPAAL

Abstract

Conference

Access to Document

Other files and links

Fingerprint

Cite this