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:
- 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;
- PKT describes all actions performed by a node when a data packet is received;
- RREQ models all events occurring when a route request is handled;
- RREP describes the reaction of the protocol to an incoming route reply;
- RERR models the part of AODVv2 which handles error messages.In particular, it describes the modification and forwarding of error message; and finally,
- 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
of natural numbers is used to describe the distances between nodes, it could be replaced by any other (monotonically increasing) metric. The set
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:
- the target IP address, which is an element of IP;
- the target sequence number—an element of SQN;
- the next hop, which is again an element of IP;
- the route-forwarding flag—a Boolean value;
- the route-broken flag—a Boolean value;
- the distance to the destination, an element of
.
We make use of the standardfunction +1.
The functions
![projection](math/pi.png)
(
![](math/pi2.png)
) denotes the projection to the
![i](math/i.png)
-th component of a routing table entry. For example
![projection1](math/pi1.png)
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](math/RT_def.png)
Complex Types: Next to [
TYPE] and
![powerset ofIP](math/pow_ip.png)
, 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](math/unodes_type.png)
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,
![function type inodes](math/inodes_type.png)
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
![function type head](math/head_type.png)
and
![function type tail](math/tail_type.png)
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](math/fnselq.png)
,
![functionname sigma_p_flag](math/fnselp.png)
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](math/selroute.png)
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](math/pi1_6.png)
we can select the components of any chosen entry:
- The target sequence number relative to tip:
![definition sqn](math/sqn.png)
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. - The address of the next hop on a route to tip:
![definition nhop](math/nhop.png)
- The route-forwarding flag of a route:
![definition forward flag](math/fwf.png)
- The route-broken flag of a route:
![definition broken flag](math/brf.png)
- The distance of the route from the current node to tip:
![definition dist](math/dist.png)
To keep the distances to intermediate nodes up to date, they have to be incremented regularly.
![definition distinc](math/distinc.png)
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
![definition upd_route](math/upd_r.png)
The definition follows the description given in Sect. 5.2.1. of
[2].
2The 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:
![definition upd_inter](math/updinter.png)
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](math/update.png)
To invalidate routing table entries we use the following functions.
![definition invalidate](math/invalidate.png)
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](math/msgs.png)
The data structure is summarised in the following table.
B. Processes
The Basic Routine:
![The Base Routine](dymo.jpg)
Packet Handling:
![Packet Handling](pkt.jpg)
Route Request Handling:
![RREQ Handling](rreq.jpg)
Route Reply Handling:
![RREP Handling](rrep.jpg)
Route Error Handling:
![RERR Handling](rerr.jpg)
Message Queue:
AODVv2 Modelled in UPPAAL
The Uppaal can be found here. | ![Uppaal model](dymo_upp.jpg) |
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. |
Contact: Peter Höfner: peter <at> hoefner-online.de
Last update: Aug. 01, 2012