Statistical Model Checking of Wireless Mesh Routing Protocols

P. Höfner, A. McIver

Abstract: Several case studies indicate that model checking is limited in the analysis of mesh networks: state space explosion restricts applicability to at most 10 node networks, and quantitative reasoning, often sufficient for network evaluation, is not possible. Both deficiencies can be overcome to some extent by the use of statistical model checkers, such as SMC-Uppaal. In this paper we illustrate this by a quantitative analysis of two well-known routing protocols for wireless mesh networks, namely AODV and DYMO. Moreover, we push the limits and show that this technology is capable of analysing networks of up to 100 nodes.

Paper: pdf

Architecture of AODV and DYMO

Our models for AODV and DYMO follow the same basic architecture in the network protocol layer. Each node maintains a message queue to store incoming messages and a processor for handling messages. Whilst the message queue is always enabled to receive messages, message handling can take time and so communication between queue and handler occurs only when the handler has successfully processed a message. The workflow of the handler is as follows: first, the next (oldest) message is loaded from its message queue. Depending on the type of message the routing table is updated and, if necessary, a new message is created, and either broadcast or unicast.

The Uppaal and SMC-Uppaal models can be downloaded here:
AODV
Image of the Handler:img1		DYMO
Image of the Handler:img2


Experiments

The experiments performed can be split into four categories:
  1. a timing analysis of AODV;
  2. a comparison between AODV and DYMO;
  3. a quantitative analysis of the two protocols; and
  4. a feasibility study of networks of realistic size.
The experiments of the first three categories were performed in the following setup: 3.1GHz Intel Pentium 5 CPU, with 16GB memory, running the Mac OS X 10.7 operating system. For our final experiment we needed 128GB memory (3.3GHz). In all our experiments we used the Statistical Model-Checker Extension of Uppaal 4.1.11 (June 2012).

A Timing Analysis of AODV

We performed the same experiments for DYMO. Here we present the graphical results for network topologies of size 3, 4 and 5.

3-Node Topologies
img3img4img5
(a) running time of AODV(b) route establishment(c) combined properties
par: "
4-Node Topologies
img6img7img8
(a) running time of AODV(b) route establishment(c) combined properties


5-Node Topologies
img9img10img11
(a) running time of AODV(b) route establishment(c) combined properties

A Timing Analysis of DYMO

Here we only present the graphical results for network topologies of size 3, 4 and 5. A detailed description can be found in the paper.

3-Node Topologies
img12img13img14
(a) running time of DYMO(b) route establishment(c) combined properties


4-Node Topologies
img15img16img17
(a) running time of DYMO(b) route establishment(c) combined properties


5-Node Topologies
img18img19img20
(a) running time of DYMO(b) route establishment(c) combined properties

AODV versus DYMO

To our surprise, the variation in performance between the two is marginal. A graphical comparison is given in the following graphics.

3-Node Topologies
img21img22img23
(a) running time(b) route establishment(c) combined properties


4-Node Topologies
img24img25img26
(a) running time(b) route establishment(c) combined properties


5-Node Topologies
img27img28img29
(a) running time(b) route establishment(c) combined properties

DYMO establishes fewer routes than AODV

The experiments performed showed that in average DYMO establishes fewer routes (compared to AODV). In this section we present an example. It is not an example we generate in the paper, but we tried to find an example that is easy to understand and which does not need too much knowledge about the protocols itself.

Assume the following topology. (The small numbers in the nodes indicate the nodes' sequence numbers.)

img30
Initial State.

In our scenario, node A is first looking for a route to C, followed by node B looking for D.


We first show the behaviour of AODV:

The presented routing table entries have the form (destination, sequence number, valid destination sequence number flag, validity flag, hop count, next hop).
AODV
   img31(a) Node A initiates a route RREQ,
  which is broadcast to B.		   img32(b) Node B updates its routing table and
  forwards the RREQ1.		   img33(c) At the same time B is handling RREQ1,
  node D initiates a route request destined for B.
   img34(d) Node replies to RREQ1 with a reply,
  unicast to B.		   img35(e) Parts (e) and (f) happen at the same time.
  Node B forwards the reply RREP1.		   img36(f) Node C handles RREQ2;it has only a
   route with unknown sequence number;
  it must broadcast it to nodes B, D and E.
   img37(g) E forwards RREQ2.
   img38(h) At the same time B generates a reply;
  it forwards RREP2 to C.		   img39(i) Node C forwards RREP2.
After the protocol (AODV) has terminated, 13 routes have been established.


Let us now look at DYMO.

The presented routing table entries have the form (destination, sequence number, route.broken flag, hop count, next hop).
DYMO
   img40(a) Node A initiates a route RREQ,
  which is broadcast to B.		   img41(b) Node B updates its routing table and
  forwards the RREQ1.		   img42(c) At the same time B is handling RREQ1,
  node D initiates a route request destined for B.
   img43(d) Node replies to RREQ1 with a reply,
  increments its SQN and unicasts RREP1.		   img44(e) Parts (e) and (f) happen at the same time.
  Node B forwards the reply RREP1.		   img45(f) Node C handles RREQ2;thanks to
   route accumulation it has a valid route to B;
  it send replies to B and D.
  That is the end of the protocol.

Note that node E is not establishing ANY route and also node C established fewer routes than in the case of AODV.. In total, DYMO established 10 routes, 3 less than AODV.

Contact: Peter Höfner: peter.hoefner <at> nicta.com.au

Last update: 2013