Formal Methods for Wireless Mesh Network Routing Protocols @ SSRG
—Specification, Verification and Analysis—
Aim: improve reliability and performance of standard routing protocols for wireless mesh networks
 |
Wireless Mesh Networks (WMNs) have recently gained considerable popularity and are increasingly deployed in a wide range of application scenarios, including emergency response communication, intelligent transportation systems, mining, video surveillance, etc. WMNs are essentially self-organising wireless ad-hoc networks that can provide broadband communication without relying on a wired backhaul infrastructure. This has the benefit of rapid and low-cost network deployment. Traditionally, the main tools for evaluating and validating network protocol are simulation and test-bed experiments. The key limitations of these approaches are that they are very expensive, time consuming and non-exhaustive. As a result, protocol errors and limitations are still found many years after the definition and standardisation.
Formal methods have a great potential in helping to address this problem, and can provide valuable tools for the design, evaluation and verification of WMN routing protocols. The overall goal is to reduce the "time-to-market" for better (new or modified) WMN protocols, and to increase the reliability and performance of the corresponding networks.
The project is part of Adaptive and Verified Wireless Mesh Protocols (Mesh Protocols).
- Approach: To reach the overall goal (better reliability and better performance) we analyse standard protocols w.r.t. basic requirements such as packet delivery or loop freedom. The analysis can only be performed after a formalism for the (unambigious) description of protocols has been developed. The formalism must be flexible enough to model all behaviours of wireless mesh routing protocols such as broadcast and unicast communication, data structures, and timers. The mobility of network nodes and the resulting link losses should be modelled by probabilities. A further aim is the introduction of paramatised models.
-
Case Study:
To guarantee applicability and usability of our approach, we analyse the
Ad-hoc On Demand Distance Vector (AODV) routing protocol.
AODV [1] is a widely-used routing protocol designed for
mobile ad-hoc networks (MANETs), and is one of the four protocols currently standardised by the
IETF MANET working group.
It also forms the basis of new WMN routing protocols, including the
upcoming IEEE 802.11s wireless mesh network standard [2].
AODV is a reactive protocol: routes are established only on demand.
Moreover it is designed for wireless and mobile networks, i.e., links are in particular
unreliable and can go up and down. Due to this routes have to be
invalidated or re-established
[1] Perkins, C., Belding-Royer, E., and Das, S. Ad hoc on-demand distance vector (AODV) routing. RFC 3561 (Experimental), 2003.
[2] IEEE. Draft standard for information technology — telecommunications and information exchange between systems — LAN/MAN specific requirements — part 11: Wireless medium access control (MAC) and physical layer (PHY) specifications: Amendment 10: Mesh networking, Dec. 2009. IEEE unapproved draft. -
People: Annabelle McIver, Marius Portmann, Wee Lum Tan
Collaboration: Amsterdam, Augsburg, Braunschweig, Cambridge, Dublin, Edinburgh, Shanghai, Stanford, ....
People
Activities
Since October 2010 we tackle the challenge of specifying, verifyingn and analysing wireless mesh protocols.
- Process Algebra: development of a process algebra for wireless mesh networks that combines all features needed such as novel treatments of local broadcast, conditional unicast and data structures. In this framework, we modelled the Ad-hoc On- Demand Distance Vector routing protocol.
- Model Checking: we complement the process algebraic approach by model checking. Model checking allows the confirmation and detailed diagnostics of suspected errors which arise during modelling. The availability of an executable model will become especially useful in the evaluation of proposed improvements to AODV.
- Routing algebra: it is known that simple routing protocols, such as Dijkstra's shortest path algorithm, can be formulated using concepts from linear algebra such as matrices. This enables an analysis with off-the-shelf ATP systems (automated theorem provers) and the use of standard programs like Maple to simulate protocols.
Selected Publications
2012
- A Process algebra for Wireless Mesh Networks used for Modelling, Verifying and Analysing AODV.
A. Fehnker, R.J. van Glabbeek, P. Höfner, A. McIver, M. Portmann and W. L. Tan.
Technical report, NICTA. (to appear)
draft available at http://www.nicta.com.au/__data/assets/pdf_file/0006/29292/MeshTR2011.pdf- A Process Algebra for Wireless Mesh Networks.
A. Fehnker, R.J. van Glabbeek, P. Höfner, A. McIver, M. Portmann and W. L. Tan.
In European Symposium on Programming,
Lecture Notes in Computer Science, Springer, 2012. (to appear)- Automated Analysis of AODV using UPPAAL.
A. Fehnker, R.J. van Glabbeek, P. Höfner, A. McIver, M. Portmann and W. L. Tan.
In Tools and Algorithms for the Construction and Analysis of Systems,
Lecture Notes in Computer Science, Springer, 2012. (to appear)2011
- Modelling and Analysis of AODV in UPPAAL.
A. Fehnker, R.J. van Glabbeek, P. Höfner, A. McIver, M. Portmann and W. L. Tan.
In International Workshop on Rigorous Protocol Engineering, 2011.- Towards an Algebra of Routing Tables.
P. Höfner and A. McIver.
In H. de Swart (ed.), Relational and Algebraic Methods in Computer Science,
Lecture Notes in Computer Science 6663, 212-229, Springer, 2011.