Modelling and verifying the AODV routing protocol

Rob van Glabbeek; Peter Höfner; Marius Portmann; Wee Lum Tan

doi:10.1007/s00446-015-0262-7

Modelling and verifying the AODV routing protocol

Rob van Glabbeek, Peter Höfner^*, Marius Portmann, Wee Lum Tan

^*Corresponding author for this work

Research output: Contribution to journal › Article › peer-review

44 Citations (Scopus)

Abstract

This paper presents a formal specification of the Ad hoc On-demand Distance Vector (AODV) routing protocol using AWN (Algebra for Wireless Networks), a recent process algebra which has been tailored for the modelling of mobile ad hoc networks and wireless mesh network protocols. Our formalisation models the exact details of the core functionality of AODV, such as route discovery, route maintenance and error handling. We demonstrate how AWN can be used to reason about critical protocol properties by providing detailed proofs of loop freedom and route correctness.

Original language	English
Pages (from-to)	279-315
Number of pages	37
Journal	Distributed Computing
Volume	29
Issue number	4
DOIs	https://doi.org/10.1007/s00446-015-0262-7
Publication status	Published - 1 Aug 2016
Externally published	Yes

Access to Document

10.1007/s00446-015-0262-7

Cite this

@article{ced57cd3fb5446d7aecb390a51afb232,

title = "Modelling and verifying the AODV routing protocol",

abstract = "This paper presents a formal specification of the Ad hoc On-demand Distance Vector (AODV) routing protocol using AWN (Algebra for Wireless Networks), a recent process algebra which has been tailored for the modelling of mobile ad hoc networks and wireless mesh network protocols. Our formalisation models the exact details of the core functionality of AODV, such as route discovery, route maintenance and error handling. We demonstrate how AWN can be used to reason about critical protocol properties by providing detailed proofs of loop freedom and route correctness.",

keywords = "AODV, AWN, Loop freedom, Mobile ad-hoc networks, Process algebra, Routing protocols, Wireless mesh networks",

author = "{van Glabbeek}, Rob and Peter H{\"o}fner and Marius Portmann and Tan, {Wee Lum}",

note = "Publisher Copyright: {\textcopyright} 2016, Springer-Verlag Berlin Heidelberg.",

year = "2016",

month = aug,

day = "1",

doi = "10.1007/s00446-015-0262-7",

language = "English",

volume = "29",

pages = "279--315",

journal = "Distributed Computing",

issn = "0178-2770",

publisher = "Springer Verlag",

number = "4",

}

TY - JOUR

T1 - Modelling and verifying the AODV routing protocol

AU - van Glabbeek, Rob

AU - Höfner, Peter

AU - Portmann, Marius

AU - Tan, Wee Lum

PY - 2016/8/1

Y1 - 2016/8/1

N2 - This paper presents a formal specification of the Ad hoc On-demand Distance Vector (AODV) routing protocol using AWN (Algebra for Wireless Networks), a recent process algebra which has been tailored for the modelling of mobile ad hoc networks and wireless mesh network protocols. Our formalisation models the exact details of the core functionality of AODV, such as route discovery, route maintenance and error handling. We demonstrate how AWN can be used to reason about critical protocol properties by providing detailed proofs of loop freedom and route correctness.

AB - This paper presents a formal specification of the Ad hoc On-demand Distance Vector (AODV) routing protocol using AWN (Algebra for Wireless Networks), a recent process algebra which has been tailored for the modelling of mobile ad hoc networks and wireless mesh network protocols. Our formalisation models the exact details of the core functionality of AODV, such as route discovery, route maintenance and error handling. We demonstrate how AWN can be used to reason about critical protocol properties by providing detailed proofs of loop freedom and route correctness.

KW - AODV

KW - AWN

KW - Loop freedom

KW - Mobile ad-hoc networks

KW - Process algebra

KW - Routing protocols

KW - Wireless mesh networks

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

U2 - 10.1007/s00446-015-0262-7

DO - 10.1007/s00446-015-0262-7

M3 - Article

SN - 0178-2770

VL - 29

SP - 279

EP - 315

JO - Distributed Computing

JF - Distributed Computing

IS - 4

ER -

Modelling and verifying the AODV routing protocol

Abstract

Access to Document

Other files and links

Fingerprint

Cite this