Skip to main content


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},
    author           = {Höfner, Peter and Kamali, Maryam},
    month            = {aug},
    editor           = {{V. Braberman and L. Fribourg}},
    year             = {2013},
    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
    booktitle        = {11th International Conference on Formal Modeling and Analysis of Timed Systems (Formats '13)},
    pages            = {15},
    address          = {Buenos Aires, Argentina}