Modelling and verifying the AODV routing protocol

DOI10.1007/S00446-015-0262-7zbMATH Open1386.68019arXiv1512.08867OpenAlexW3121942651MaRDI QIDQ324632FDOQ324632

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)

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.

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

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

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)

Cites Work

• A Mechanized Proof of Loop Freedom of the (Untimed) AODV Routing Protocol
• Title not available (Why is that?)
• Title not available (Why is that?)
• Broadcast psi-calculi with an application to wireless protocols
• Algebra of communicating processes with abstraction
• An observational theory for mobile ad hoc networks (full version)
• Towards a calculus for wireless systems
• Showing Invariance Compositionally for a Process Algebra for Network Protocols
• A process algebra for wireless mesh networks
• A Calculus for Mobile Ad Hoc Networks
• A framework for security analysis of mobile wireless networks
• A process calculus for mobile ad hoc networks
• Simulation-based performance evaluation of routing protocols for mobile ad hoc networks
• A Timed Process Algebra for Wireless Networks with an Application in Routing
• Title not available (Why is that?)
• Formal verification of standards for distance vector routing protocols

Cited In (12)

• Formal verification of secure ad hoc routing protocols using AVISPA: ARAN case study
• A Timed Process Algebra for Wireless Networks with an Application in Routing
• Modeling Routing Protocols in Adhoc Networks
• Analysing AWN-Specifications Using mCRL2 (Extended Abstract)
• Towards an algebra of routing tables
• Modelling and Initial Validation of the DYMO Routing Protocol for Mobile Ad-Hoc Networks
• Trading Plaintext-Awareness for Simulatability to Achieve Chosen Ciphertext Security
• Modeling and verifying ad hoc routing protocols
• Title not available (Why is that?)
• A process algebra for wireless mesh networks
• Modeling and efficient verification of wireless ad hoc networks
• Depletable channels: dynamics, behaviour, and efficiency in network design

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)