Quantitative analysis of AODV and its variants on dynamic topologies using statistical model checking
Authors
NICTA
UNSW
Abo Akademi University
Abstract
Wireless Mesh Networks (WMNs) are self-organising ad-hoc networks that support broadband communication. Due to changes in the topology, route discovery and maintenance play a crucial role in the reliability and the performance of such networks. Formal analysis of WMNs using exhaustive model checking techniques is often not feasible: network size (up to hundreds of nodes) and topology changes yield state- space explosion. Statistical Model Checking, however, can overcome this problem and allows a quantitative analysis. In this paper we illustrate this by a careful analysis of the Ad hoc On-demand Distance Vector (AODV) protocol. We show that some optional features of AODV are not useful, and that AODV shows unexpected behaviour - yielding a high probability of route discovery failure.
BibTeX Entry
@inproceedings{Hoefner_Kamali_13, address = {Buenos Aires, Argentina}, author = {H\"ofner, Peter and Kamali, Maryam}, booktitle = {International Conference on Formal Modeling and Analysis of Timed Systems}, editor = {{V. Braberman and L. Fribourg}}, keywords = {statistical model checking; wireless mesh networks; routing protocols; quantitative analysis; case study}, month = aug, pages = {15}, paperurl = {https://trustworthy.systems/publications/nicta_full_text/6678.pdf}, publisher = {Springer}, title = {Quantitative Analysis of {AODV} and its Variants on Dynamic Topologies using Statistical Model Checking}, year = {2013} }