Skip to main content
Department of Information Technology

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.
ad_hoc_net.jpg

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.

Related Work

Publications

A Testbed for Evaluating Delay Tolerant Network Protocol Implementations. Fredrik Bjurefors and Oskar Wibling. In Proceedings 5th Swedish National Computer Networking Workshop, 2008.
Creating Correct Network Protocols. Oskar Wibling. Ph.D. thesis, Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology nr 571, Acta Universitatis Upsaliensis, Uppsala, 2008. (fulltext, errata).
Graph Grammar Modeling and Verification of Ad Hoc Routing Protocols. Mayank Saksena, Oskar Wibling, and Bengt Jonsson. In Tools and Algorithms for the Construction and Analysis of Systems, volume 4963 of Lecture Notes in Computer Science, pp 18-32, Springer-Verlag, Berlin, 2008. (DOI).
Evaluating Wireless Multi-hop Networks Using a Combination of Simulation, Emulation, and Real World Experiments. Erik Nordström, Per Gunningberg, Christian Rohner, and Oskar Wibling. In Proceedings of the 1st international workshop on System evaluation for mobile platforms (MobiEval'07), pp 29-34, ACM Association for Computing Machinery, New York, 2007. (DOI).
Ad Hoc Routing Protocol Verification Through Broadcast Abstraction. Oskar Wibling, Joachim Parrow, and Arnold Pears. In Formal Techniques for Networked and Distributed Systems – FORTE 2005, volume 3731 of Lecture Notes in Computer Science, pp 128-142, Springer-Verlag, Berlin, 2005. (DOI).
Ad hoc routing protocol validation. Oskar Wibling. Licentiate thesis, IT licentiate theses / Uppsala University, Department of Information Technology nr 2005-004, Uppsala University, 2005. (fulltext).
Automatized Verification of Ad Hoc Routing Protocols. Oskar Wibling, Joachim Parrow, and Arnold Pears. In Formal Techniques for Networked and Distributed Systems – FORTE 2004, volume 3235 of Lecture Notes in Computer Science, pp 343-358, Springer-Verlag, Berlin, 2004. (DOI).
LUNAR - A Lightweight Underlay Network Ad-hoc Routing Protocol and Implementation. Christian Tschudin, Richard Gold, Olof Rensfelt, and Oskar Wibling. In Next Generation Teletraffic and Wired/Wireless Advanced Networking (NEW2AN'04), p 300, 2004.

Updated  2016-08-17 15:26:28 by Björn Victor.