Modelling and verifying the AODV routing protocol

DOI10.1007/S00446-015-0262-7MaRDI QIDQ324632zbMATHOpenAlexFDO

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

Publication date 17 October 2016

Published in Distributed Computing (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1512.08867

zbMATH Keywords

process algebrawireless mesh networksAODVAWNloop freedommobile ad-hoc networksrouting protocols

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Network protocols (68M12)

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.

Recommendations

• Modeling Routing Protocols in Adhoc Networks
• Probabilistic model checking of AODV
• Modelling and Initial Validation of the DYMO Routing Protocol for Mobile Ad-Hoc Networks
• A process algebra for wireless mesh networks
• Formal verification of secure ad hoc routing protocols using AVISPA: ARAN case study

Cites work

• scientific article; zbMATH DE number 2088547 (Why is no real title available?)
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• A Calculus for Mobile Ad Hoc Networks
• A framework for security analysis of mobile wireless networks
• A mechanized proof of loop freedom of the (untimed) AODV routing protocol
• A process algebra for wireless mesh networks
• A process calculus for mobile ad hoc networks
• A timed process algebra for wireless networks with an application in routing (extended abstract)
• Algebra of communicating processes with abstraction
• An observational theory for mobile ad hoc networks (full version)
• Broadcast psi-calculi with an application to wireless protocols
• Formal verification of standards for distance vector routing protocols
• Showing invariance compositionally for a process algebra for network protocols
• Simulation-based performance evaluation of routing protocols for mobile ad hoc networks
• Towards a calculus for wireless systems

Cited in

(14)

• Analysing AWN-Specifications Using mCRL2 (Extended Abstract)
• Formal verification of secure ad hoc routing protocols using AVISPA: ARAN case study
• A process algebra for wireless mesh networks
• A mechanized proof of loop freedom of the (untimed) AODV routing protocol
• Towards an algebra of routing tables
• scientific article; zbMATH DE number 2202252 (Why is no real title available?)
• Probabilistic model checking of AODV
• Depletable channels: dynamics, behaviour, and efficiency in network design
• Trading plaintext-awareness for simulatability to achieve chosen ciphertext security
• Modeling Routing Protocols in Adhoc Networks
• Modelling and Initial Validation of the DYMO Routing Protocol for Mobile Ad-Hoc Networks
• Modeling and efficient verification of wireless ad hoc networks
• A timed process algebra for wireless networks with an application in routing (extended abstract)
• Modeling and verifying ad hoc routing protocols

Describes a project that uses

Uses Software

• LOTOS
• HOL/SPIN
• ns-2
• QualNet
• AODV

This page was built for publication: Modelling and verifying the AODV routing protocol

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q324632)