@inproceedings{100b125822f34ef2b4293fb0f3e62360,
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.",
author = "Xiaofeng Wu and Qiwen Xu and Huibiao Zhu",
year = "2013",
doi = "10.1109/TASE.2013.14",
language = "英语",
isbn = "9780768550534",
series = "Proceedings - 2013 International Symposium on Theoretical Aspects of Software Engineering, TASE 2013",
pages = "45--48",
booktitle = "Proceedings - 2013 International Symposium on Theoretical Aspects of Software Engineering, TASE 2013",
note = "2013 International Symposium on Theoretical Aspects of Software Engineering, TASE 2013 ; Conference date: 01-07-2013 Through 03-07-2013",
}