Trustworthy Systems

Quantitative analysis of AODV and its variants on dynamic topologies using statistical model checking

Authors

Peter Hoefner and Maryam Kamali

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}
  }

Download