Descriptions of Mobile Ad-hoc Networks

Motivation

Existing approaches to evaluate protocols for ad hoc and intermittently connected networks mainly test protocols using simulations. This provides quantitative insights into protocol behavior but cannot guarantee correct operation in all situations. In many cases correct application of formal methods during protocol design would have increased system reliability. Formal verification studies of the AODV ad hoc routing protocol have, for instance, detected routing loops, and problems with route lifetimes in large diameter networks.

Our motivation is thus two-fold:

• To develop new and simplified methodologies for ad hoc protocol analysis using formal methods, including tool support. This will make the techniques more easily adopted and more widely used.
• Extending the body of knowledge of network protocol properties through the modeling and verification of existing ad hoc protocol designs and proposals.

Approach

We initially performed studies where we modeled and verified correct operation of the LUNAR protocol in finite networks, using model checking. This is an automatized approach which requires the user to specify the protocol using a high level formalism and provide some general properties. These are then given to a model checking tool which outputs a pass or fail answer to questions regarding key protocol properties, without involving the user in additional interaction.

Even when sound abstractions are manually introduced (e.g., our broadcast abstraction, see below) there is still a significant limitation in the size of networks and number of topology changes that can be introduced before running into state space explosion. Besides verifying relevant properties of ad hoc protocols we want to come as close as possible to push button verification in order for protocol designers to be able to routinely perform this task on new protocols. Therefore, we are now investigating ways to make infinite state verification methods more accessible to the protocol designers.

Results

The modeling and verification of the ad hoc routing properties of LUNAR has yielded experience regarding creation of protocol models, and helped to identify limitations with existing verification approaches and tools. The protocol has been analyzed using tools like SPIN and UPPAAL. See the NEW2AN'04 and FORTE'04 papers below for results. Through broadcast abstraction we were able to extend the analysis to networks of realistic sizes, results which were presented at FORTE'05 (see below). However, the possible topological changes were still limited, and strong assumptions regarding network configurations were needed to show correct routing. In contrast, our work on verification using graph grammar models has enabled us to prove loop freedom of the DYMO protocol automatically. The result is valid for an arbitrary number of nodes and topology changes.

Resources

Our tool for graph grammar verification, the Graph Backwards Tool (GBT), can be found here.

Ongoing Work

At present [Jan 2008], we are working on the following two topics.

• Modeling and verification of ad hoc routing protocols using graph grammars. We have developed the GBT tool for this purpose.
• Applying probabilistic model checking to ad hoc protocols.

Related Work

• Obradovic et al used the SPIN model checker and the HOL theorem prover to verify route validity and freedom from routing loops in AODV.
• Das and Dill also proved absence of routing loops in a simplified version of AODV. They used predicate abstraction and discovered quantified predicates automatically by analyzing spurious abstract counter-example traces.
• Lahiri and Bryant also verified loop freedom of AODV using predicate abstraction in their tool called UCLID PA.
• Chiyangwa and Kwiatkowska studied timing properties of AODV using UPPAAL.
• de Renesse and Aghvami used SPIN to model check the ad hoc routing protocol WARP.

Publications