USP Electronic Research Repository

Automated analysis of AODV using UPPAAL

Fehnker, Ansgar and van Glabbeek, R.J. and Hoefner, P. and McIver, A. and Portmann, M. and Tan, W.L. (2012) Automated analysis of AODV using UPPAAL. [Conference Proceedings]

PDF - Accepted Version
Download (374Kb) | Preview


    This paper describes an automated, formal and rigorous analysis of the Ad hoc On-Demand Distance Vector (AODV) routing protocol, a popular protocol used in wireless mesh networks. We give a brief overview of a model of AODV implemented in the UPPAAL model checker. It is derived from a process-algebraic model which reflects precisely the intention of AODV and accurately captures the protocol specification. Furthermore, we describe experiments carried out to explore AODV's behaviour in all network topologies up to 5 nodes. We were able to automatically locate problematic and undesirable behaviours. This is in particular useful to discover protocol limitations and to develop improved variants. This use of model checking as a diagnostic tool complements other formal-methods-based protocol modelling and verification techniques, such as process algebra.

    Item Type: Conference Proceedings
    Subjects: Q Science > QA Mathematics > QA75 Electronic computers. Computer science
    Divisions: Faculty of Science, Technology and Environment (FSTE) > School of Computing, Information and Mathematical Sciences
    Depositing User: Ansgar Fehnker
    Date Deposited: 01 May 2013 15:48
    Last Modified: 25 Jul 2016 14:25

    Actions (login required)

    View Item

    Document Downloads

    More statistics for this item...