Descriptions of Mobile Ad-hoc Networks

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.

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.

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

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.

• 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.