Formal Analysis of AODV Using Rely-Guarantee

Author

Xiaofeng Wu ; Qiwen Xu ; Huibiao Zhu

Author_Institution

Shanghai Key Lab. of Trustworthy Comput., East China Normal Univ., Shanghai, China

fYear

2013

fDate

1-3 July 2013

Firstpage

45

Lastpage

48

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.

Keywords

mobile ad hoc networks; parallel programming; routing protocols; telecommunication computing; AODV routing protocol formal Analysis; Ad-hoc On-Demand Distance Vector routing protocol; MANET; infrastructureless scenarios; mobile ad-hoc networks; network connections; program parallel component; rely-guarantee method; route discovery process specification; shared-variable concurrent program; Ad hoc networks; Mobile computing; Receivers; Routing; Routing protocols; Vectors;

fLanguage

English

Publisher

ieee

Conference_Titel

Theoretical Aspects of Software Engineering (TASE), 2013 International Symposium on

Conference_Location

Birmingham

Type

conf

DOI

10.1109/TASE.2013.14

Filename

6597876