Automated Analysis of AODV using UPPAAL
arXiv:1512.07352 · doi:10.1007/978-3-642-28756-5_13
Abstract
This paper describes an automated, formal and rigorous analysis of the Ad hoc On-Demand Distance Vector (AODV) routing protocol, a popular protocol used in wireless mesh networks. We give a brief overview of a model of AODV implemented in the UPPAAL model checker. It is derived from a process-algebraic model which reflects precisely the intention of AODV and accurately captures the protocol specification. Furthermore, we describe experiments carried out to explore AODV's behaviour in all network topologies up to 5 nodes. We were able to automatically locate problematic and undesirable behaviours. This is in particular useful to discover protocol limitations and to develop improved variants. This use of model checking as a diagnostic tool complements other formal-methods-based protocol modelling and verification techniques, such as process algebra.
arXiv admin note: text overlap with arXiv:1512.07312
References in corpus (1)
Cited by in corpus (9)
- Automated Analysis of AODV using UPPAAL
- Modelling and Verifying the AODV Routing Protocol
- Sequence Numbers Do Not Guarantee Loop Freedom; AODV Can Yield Routing Loops
- Model Checking Paxos in Spin
- Modelling, Verification, and Comparative Performance Analysis of the B.A.T.M.A.N. Protocol
- Formalising the Optimised Link State Routing Protocol
- Advanced Models for the OSPF Routing Protocol
- Formal Models of the OSPF Routing Protocol
- Graph- versus Vector-Based Analysis of a Consensus Protocol