Towards a Rigorous Analysis of AODVv2 (DYMO)

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

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 .
   We make use of the standardfunction +1.

The functions () denotes the projection to the -th component of a routing table entry. For example 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.¹ Formally, we define the type RT of routing tables by

Complex Types:
Next to [TYPE] and , 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.
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

.

Since both characterisations (sets and partial functions) are isomorphic we make freely use of both.
Similar to the set of unreachable destination, describes a set of intermediate destinations. Each destination is equipped with the last-known sequence number as well as the distance to the node.

Functions:
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 and 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, , 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.

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 we can select the components of any chosen entry:

1. The target sequence number relative to tip:

   

   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:

   

3. The route-forwarding flag of a route:

   

4. The route-broken flag of a route:

   

5. The distance of the route from the current node to tip:

   

To keep the distances to intermediate nodes up to date, they have to be incremented regularly.

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.

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

The definition follows the description given in Sect. 5.2.1. of [2].²
The function distinguishes four cases:

• if the incoming sequence number tsn is smaller than the one stored in the route r, the new information is stale and must be disregarded;
• if the incoming sequence number is equal to the one stored in the route and one of the following three cases holds, the new information is loop possible and must be disregarded: (i) the incoming distance tdist is greater or equal to the one stored (ii) the incoming distance is 0, i.e., not known (iii) the stored distance is 0, i.e. not known;
• if the incoming sequence number is identical to the one stored in the route and one of the following two cases holds, the new information is disfavoured or equivalent and is therefore discarded: (i) the incoming distance is larger than the one stored for the route and the route is not broken, i.e., the route broken flag is set false (ii) the incoming distance is equal to the one stored, the message is a route request and the route is not broken;
• in any other case, the new information is preferable and therefore should be added to the routing table of tip with the route forwarding flag set true and the route broken flag set false.

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:

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

To invalidate routing table entries we use the following functions.

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

B. Processes

AODVv2 Modelled in UPPAAL

The Uppaal can be found here.

References

[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, http://www.nicta.com.au/pub?id=5513.
[2]	C. Perkins and I. Chakeres, “Dynamic MANET on-demand (AODVv2) routing”, IETF Internet Draft, March 2012, (Work in Progress). Available: http://tools.ietf.org/html/draft-ietf-manet-dymo-22.

---

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.