@inproceedings{53915d174e41498989c0c6c1bf6a2c8d,
title = "Formal modelling and analysis of AODV",
abstract = "Wireless systems have a wide range of applications recently. To explore complex features of such systems, formalisms are proposed to specify and reason about them. This paper presents a case study of routing protocol in wireless networks. We formalize the route discovery process of AODV routing protocol using Object-Z. Network topology and local variables of nodes are defined by relations and functions. The broadcast communication is modelled by operations which change local variables of the sender and all of its connected receivers simultaneously. We show the proof of loop freedom property for established routes based on the specification. Further, the specification is modified by adding mobility of nodes and loop freedom under a dynamic network topology is discussed, showing the scalability of our approach.",
author = "Xiaofeng Wu and Sanders, \{J. W.\} and Huibiao Zhu",
year = "2013",
doi = "10.1109/ICECCS.2013.22",
language = "英语",
isbn = "9780769550077",
series = "Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "93--100",
booktitle = "Proceedings - 2013 International Conference on Engineering of Complex Computer Systems, ICECCS 2013",
address = "美国",
note = "18th International Conference on Engineering of Complex Computer Systems, ICECCS 2013 ; Conference date: 17-07-2013 Through 19-07-2013",
}