Skip to main content

Formal Methods for Wireless Networks

Formal Methods for Wireless Networks
—Specification, Verification and Analysis—

  • Aim: improve reliability and performance of standard routing protocols for wireless mesh networks



  • Context: 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, disaster recovery, 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 protocols 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.
  • Approach: The project explores new Formal Methods based techniques, which can provide powerful new tools for the design and evaluation of protocols and can provide critical assurance about protocol correctness and performance. 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 (unambiguous) 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 parametrised 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 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. 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, 2011.
  • Collaboration: Macquarie University, University of Queensland, INRIA, University of South Pacific, Turku Centre for Computer Science (TUCS), and Åbo Akademi University

People

Current

Past

  • Emile Bres
  • Matthias Daum
  • Ansgar Fehnker
  • Maryam Kamali
  • Tran Ngoc Ma

Activities

  • Process Algebra: development of a process algebra for wireless mesh networks that combines all features needed, such as treatments of local broadcast, conditional unicast and data structures. This framework yields unambigous specifications and allows formal reasoning to guarantee protocol properties, such as loop freedom of the AODV routing protocol.
  • Isabelle/HOL: to increase trust of the pen-and-paper proofs done in the above mentioned process algebra, we use the interactive theorem prover Isabelle/HOL to mechanise them. As a result the proofs will be machine checked.
  • 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 becomes especially useful in the evaluation of proposed improvements to AODV. In case model checking cannot succeed due to state space explosion, we also apply statistical model checking. This approach also allows a quantitative analysis of the protocols.
  • 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.

Publications

2016

Abstract PDF Rob van Glabbeek, Peter Hoefner, Marius Portmann and Wee Lum Tan
Modelling and verifying the AODV routing protocol
Distributed Computing, Volume 29, Number 4, pp. 279-315, August, 2016
Abstract PDF Emile Bres, Rob van Glabbeek and Peter Hoefner
A timed process algebra for wireless networks with an application in routing (extended abstract)
European Symposium on Programming, pp. 95-122, Eindhoven, The Netherlands, April, 2016
Abstract PDF Timothy Bourke, Rob van Glabbeek and Peter Hoefner
Mechanizing a process algebra for network protocols
Journal of Automated Reasoning, Volume 56, Number 3, pp. 309-341, March, 2016
Abstract PDF Emile Bres, Rob van Glabbeek and Peter Hoefner
A timed process algebra for wireless networks with an application in routing
Technical Report, NICTA, February, 2016

2015

Abstract PDF Peter Hoefner
Using process algebra to design better protocols (abstract)
Forum “Math-for-Industry” 2015, pp. 31-33, Fukuoka, Japan, October, 2015
Abstract PDF Mojgan Kamali, Peter Hoefner, Maryam Kamali and Luigia Petre
Formal analysis of proactive, distributed routing
Software Engineering and Formal Methods, pp. 15, York, UK, September, 2015

2014

Abstract PDF Timothy Bourke, Rob van Glabbeek and Peter Hoefner
A mechanized proof of loop freedom of the (untimed) AODV routing protocol
International Symposium on Automated Technology for Verification and Analysis (ATVA), pp. 47-63, Sydney, Australia, November, 2014
Abstract PDF Timothy Bourke, Rob van Glabbeek and Peter Hoefner
Showing invariance compositionally for a process algebra for network protocols
International Conference on Interactive Theorem Proving, pp. 44-59, Vienna, Austria, July, 2014
Abstract PDF Peter Hoefner and Annabelle McIver
Hopscotch—reaching the target hop by hop
Journal of Logical and Algebraic Methods in Programming (JLAMP), Volume 83, Number 2, pp. 212-224, April, 2014

2013

Abstract PDF Ansgar Fehnker, Rob van Glabbeek, Peter Hoefner, Annabelle McIver, Marius Portmann and Wee Lum Tan
A process algebra for wireless mesh networks used for modelling, verifying and analysing AODV
Technical Report 5513, NICTA, December, 2013
Abstract PDF Rob van Glabbeek, Peter Hoefner, Wee Lum Tan and Marius Portmann
Sequence numbers do not guarantee loop freedom - AODV can yield routing loops
16th ACM International Conference on Modeling, Analysis and Simulation of Wireless and Mobile Systems, pp. 91-100, Barcelona, Spain, November, 2013
Abstract PDF Ansgar Fehnker, Peter Hoefner, Maryam Kamali and Vinay Mehta
Topology-based mobility models for wireless networks
10th International Conference on Quantitative Evaluation of SysTems (QEST 2013), pp. 16, Buenos Aires, Argentina, August, 2013
Abstract PDF Peter Hoefner and Maryam Kamali
Quantitative analysis of AODV and its variants on dynamic topologies using statistical model checking
11th International Conference on Formal Modeling and Analysis of Timed Systems (Formats '13), pp. 15, Buenos Aires, Argentina, August, 2013
Abstract PDF Peter Hoefner and Annabelle McIver
Statistical model checking of wireless mesh routing protocols
5th NASA Formal Methods Symposium (NFM 2013), pp. 15, Moffett Field, CA, USA, May, 2013

2012

Abstract PDF Peter Hoefner and Sarah Edenhofer
Towards a rigorous analysis of AODVv2 (DYMO)
2nd International Workshop on Rigorous Protocol Engineering (WRiPE 2012), pp. 1-6, Austin, Texas, October, 2012
Abstract PDF Peter Hoefner, Rob van Glabbeek, Wee Lum Tan, Marius Portmann, Annabelle McIver and Ansgar Fehnker
A rigorous analysis of AODV and its variants
15th ACM/IEEE International Conference on Modelling, Analysis and Simulation of Wireless and Mobile Systems (MSWIM 2012), pp. 203-212, Paphos, Cyprus, October, 2012
Abstract PDF Peter Hoefner
Kleene modules for routing procedures
Abstract, Workshop on Lattices and Relations, August, 2012.
Abstract PDF Peter Hoefner and Bernhard Möller
Dijkstra, Floyd and Warshall meet Kleene
Formal Aspects of Computing (FAOC), Volume 24, Number 4-6, pp. 459-476, July, 2012
Abstract PDF Ansgar Fehnker, Rob van Glabbeek, Peter Hoefner, Annabelle McIver, Marius Portmann and Wee Lum Tan
A process algebra for wireless mesh networks
22nd European Symposium on Programming (ESOP 2012), pp. 295-315, Tallinn, Estonia, March, 2012
Abstract PDF Ansgar Fehnker, Rob van Glabbeek, Peter Hoefner, Annabelle McIver, Marius Portmann and Wee Lum Tan
Automated analysis of AODV using UPPAAL
18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012), pp. 173-187, Tallinn, Estonia, March, 2012

2011

Abstract PDF Ansgar Fehnker, Rob van Glabbeek, Peter Hoefner, Annabelle McIver, Marius Portmann and Wee Lum Tan
Modelling and analysis of AODV in UPPAAL
1st International Workshop on Rigorous Protocol Engineering, pp. 1-6, Vancouver, October, 2011
Abstract PDF Peter Hoefner and Annabelle McIver
Towards an algebra of routing tables
12th International Conference on Relational and Algebraic Methods in Computer Science, pp. 212-229, Rotterdam, Netherlands, May, 2011

Contact

Peter Höfner, peter.hoefner <at> data61.csiro.au