Trustworthy Systems

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


Peter Hoefner and Maryam Kamali



Abo Akademi University


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

    publisher        = {Springer},
    booktitle        = {11th International Conference on Formal Modeling and Analysis of Timed Systems},
    month            = aug,
    paperurl         = {},
    year             = {2013},
    editor           = {{V. Braberman and L. Fribourg}},
    keywords         = {statistical model checking; wireless mesh networks; routing protocols; quantitative analysis; case
    title            = {Quantitative Analysis of {AODV} and its Variants on Dynamic Topologies using Statistical Model
    author           = {H\"ofner, Peter and Kamali, Maryam},
    address          = {Buenos Aires, Argentina},
    pages            = {15}