Title: Formal Analysis of AODV Using Rely-Guarantee
Abstract: Mobile Ad-hoc Networks (MANETs) are increasingly deployed in infrastructureless scenarios. Routing protocol is a crucial solution for MANETs to establish network connections. This paper presents a formal description of the AODV routing protocol and analyzes its properties using relyguarantee method. In our approach the network is specified as a shared variable concurrent program, where communication is modelled by assignment on shared variables. Each parallel component of this program is a specification of route discovery process. The rely-guarantee method allows us to express and verify properties of the protocol on the basis of specifications of its constituent components.
Publication Year: 2013
Publication Date: 2013-07-01
Language: en
Type: article
Indexed In: ['crossref']
Access and Citation
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot