Towards a Rigorous Analysis of AODVv2 (DYMO)

S. Edenhofer, P. Höfner

Abstract: Dynamic MANET On-demand (AODVv2) routing, formerly known as DYMO, is a routing protocol especially designed for wireless, multi hop networks. AODVv2 determines routes in a network in an on-demand fashion.
In this paper we present a formal model of AODVv2, using the process algebra AWN. The benefit of this is two-fold: (a) the given specification is definitely free of ambiguities; (b) a formal and rigorous analysis of the routing protocol is now feasible. To underpin the latter point we also present a first analysis of the AODVv2 routing protocol. On the one hand we show that some of the problems discovered in the AODV routing protocol, the predecessor of AODVv2, have been addressed and solved. On the other hand we show that other limitations still exist; an example is the establishment of non-optimal routes. Even worse, we locate shortcomings in the AODVv2 routing protocol that do not occur in AODV. This yields the conclusion that AODVv2 is not necessarily better than AODV.

Paper: pdf

I. AODVv2 Modelled in AWN

We present a full specification of the AODVv2 protocol. The model includes a mechanism to describe the delivery of data packets; though this is not part of the protocol itself it is necessary to trigger any AODVv2 activity. Our model consists of 6 processes, named DYMO, PKT, RREQ, RREP, RERR and QMSG:
  1. DYMO reads a message from the message queue and, depending on the type of the message, calls other processes. When there is no message handling going on the process can initiate the transmission of queued data packets or generate a new route request;
  2. PKT describes all actions performed by a node when a data packet is received;
  3. RREQ models all events occurring when a route request is handled;
  4. RREP describes the reaction of the protocol to an incoming route reply;
  5. RERR models the part of AODVv2 which handles error messages.In particular, it describes the modification and forwarding of error message; and finally,
  6. QMSG concerns message handling. Whenever a control message is received, it is stored in a message queue.

A. Data Structure

Basic Types:
IP, SQN, P, DATA, STORE and MSG are identical to AODV. Details can be found in [1]. The set NN of natural numbers is used to describe the distances between nodes, it could be replaced by any other (monotonically increasing) metric. The set BB is the set of Boolean values true and false, it is used for flags.

In the sequel we describe the remaining basic data types:

MSG_TYPE describes the type of a message. It will be used in the function update to distinguish if the update is a consequence of a route request message or of a route reply message. We will use the constants req and rep.

Following the Internet-Draft [2], a routing table entry (an element of R) consists of the following 6 components:
  1. the target IP address, which is an element of IP;
  2. the target sequence number—an element of SQN;
  3. the next hop, which is again an element of IP;
  4. the route-forwarding flag—a Boolean value;
  5. the route-broken flag—a Boolean value;
  6. the distance to the destination, an element of NN.
    We make use of the standardfunction +1.
The functions projection () denotes the projection to the i-th component of a routing table entry. For example projection1 determines the target node of a given entry.

As in [1], a routing table (an element of RT) consists of a set of routing table entries, exactly one for each known destination. Thus, a routing table is defined as a set of entries, with the restriction that each has a different destination tip, i.e., the first component of each entry in a routing table is unique.1 Formally, we define the type RT of routing tables by
definition RT
Complex Types:
Next to [TYPE] and powerset ofIP, which denote the set of all queues with elements of type TYPE and the power set of IP addresses, respectively, we make use of two additional data types. Both are used to carry additional information about nodes in messages.
function type unodes is a set of unreachable destinations, each coming together with the last-known sequence number. Since the set is only allowed to have at most one entry for each destination, we write it as partial function. Alternatively, we could use
definition unodes.
Since both characterisations (sets and partial functions) are isomorphic we make freely use of both.
Similar to the set of unreachable destination, function type inodes describes a set of intermediate destinations. Each destination is equipped with the last-known sequence number as well as the distance to the node.
The specification of AODVv2 makes use of several functions. We will present the most important ones. Functions that are self-explanatory are only described in the table below, but not explained in detail. For example we make use of the standard (partial) functions function type head and function type tail without giving a formal definition.
All functions maintaining the storage of queued data packets are taken from our specification of AODV (see [1]). In particular we make use of the six functions drop, add, setP, functionname sigma_queues, functionname sigma_p_flag and qD.
We need to extract single components of a routing table for a given destination from a given routing table, if information exist. For that, we define the following partial functions.
definition sigma_route
selects the routing table entry with target tip from rt. The function is partial since there is no guarantee that a routing table to tip does exist. Through the projections pi_1...pi_6 we can select the components of any chosen entry:
  1. The target sequence number relative to tip:
    definition sqn
    Note, that this function is actually total. In case no routing table entry exists, the sequence number is set to 0, indicating an “unknown” sequence number.
  2. The address of the next hop on a route to tip:
    definition nhop
  3. The route-forwarding flag of a route:
    definition forward flag
  4. The route-broken flag of a route:
    definition broken flag
  5. The distance of the route from the current node to tip:
    definition dist
To keep the distances to intermediate nodes up to date, they have to be incremented regularly.
definition distinc
To define an update on routing tables we first have to check if there is information about a particular route in the table. For that we define a function that determines the set o of IP addresses for known routes.
definition kD
The most important functions are the ones that maintain (update or invalidate routing table entries). Looking at the internet-draft, there are two different functions for updating routing tables: the first updates the entry of a routing table w.r.t. an originator of a message received. The second updates the routing table with information provided by a list of intermediate nodes.
Both are based on a routine that judges the usefulness of routing information, i.e., given a routing table entry and new routing information, stemming from an incoming message, the quality of the new routing information has to be evaluated and a new routing table has to be constructed. For that we define
definition upd_route
The definition follows the description given in Sect. 5.2.1. of [2].2
The function distinguishes four cases:
Based on this definition we can now define update-functions working on routing tables: First a given routing table is updated with information about intermediate nodes and additional IP-address, which is the sender of the information.
The following function updinter adds the information of the set inodes to the routing table:
definition upd_inter
Updating a single routing table entry to one particular destination is a special case of this function. Note that this update is handled in the AODVv2-draft independent of updinter
definition update
To invalidate routing table entries we use the following functions.
definition invalidate
The last functions we will use in our specification are message generators. The message types used in AODVv2 are route request, route reply and route error. Next to that we also make use of data messages. Messages are generated by
definition msgs types

The data structure is summarised in the following table.

B. Processes

The Basic Routine:
The Base Routine
Packet Handling:
Packet Handling
Route Request Handling:
RREQ Handling
Route Reply Handling:
RREP Handling
Route Error Handling:
RERR Handling
Message Queue:
Message Queue

AODVv2 Modelled in UPPAAL

The Uppaal can be found here.Uppaal model


[1]A. Fehnker, R.J. van Glabbeek, P. Höfner, A. McIver, M. Portmann, and W.L. Tan, “A Process Algebra for Wireless Mesh Networks used for Modelling, Verifying and Analysing AODV”, NICTA, Technical Report 5513, 2012,
[2]C. Perkins and I. Chakeres, “Dynamic MANET on-demand (AODVv2) routing”, IETF Internet Draft, March 2012, (Work in Progress). Available:

  1. As an alternative to restricting the set, we could have defined routing tables as partial functions from IP to R, in which case it makes more sense to define an entry as a 5-tuple, not including the the destination IP as the first component.
  2. Note that our specification carries a value for the distance all the time, hence we do not need a case distinction whether the distance is known or unknown.

Contact: Peter Höfner: peter <at>

Last update: Aug. 01, 2012