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
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
2020
|
 |
Ryan Barry, Rob van Glabbeek and Peter Hoefner Formalising the optimised link state routing protocol 4th Workshop on Models for Formal Analysis of Real Systems (MARS 2020), pp. 40-71, Dublin, Ireland, April, 2020 |
|
|
|
Jack Drury, Peter Hoefner and Weiyou Wang Formal models of the OSPF routing protocol MARS2020, pp. 72–120, Dublin, Ireland, April, 2020 |
2019
|
|
|
Peter Hoefner, Rob van Glabbeek and Michael Markl A process algebra for link layer protocols European Symposium on Programming, Prague, Czech Republic, April, 2019 |
2018
|
|
|
Rob van Glabbeek, Peter Hoefner and Djurre van der Wal Analysing AWN-specifications using mCRL2 (extended abstract) 14th International Conference on integrated Formal Methods, pp. 398-418, Maynooth, September, 2018 |
2016
|
|
|
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 |
|
|
|
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 |
|
|
|
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
|
|
|
Peter Hoefner Using process algebra to design better protocols (abstract) Forum “Math-for-Industry” 2015, pp. 31–33, Fukuoka, Japan, October, 2015 |
|
|
|
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
|
|
|
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 |
|
|
|
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 |
|
|
|
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
|
|
|
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 |
|
|
|
Ansgar Fehnker, Peter Hoefner, Maryam Kamali and Vinay Mehta Topology-based mobility models for wireless networks International Conference on Quantitative Evaluation of SysTems, pp. 16, Buenos Aires, Argentina, August, 2013 |
|
|
|
Peter Hoefner and Maryam Kamali Quantitative analysis of AODV and its variants on dynamic topologies using statistical model checking International Conference on Formal Modeling and Analysis of Timed Systems, pp. 15, Buenos Aires, Argentina, August, 2013 |
|
|
|
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
|
|
|
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 |
|
|
|
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 |
|
|
|
Peter Hoefner Kleene modules for routing procedures Abstract, Workshop on Lattices and Relations, August, 2012. |
|
|
|
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 |
|
|
|
Ansgar Fehnker, Rob van Glabbeek, Peter Hoefner, Annabelle McIver, Marius Portmann and Wee Lum Tan A process algebra for wireless mesh networks European Symposium on Programming, pp. 295–315, Tallinn, Estonia, March, 2012 |
|
|
|
Ansgar Fehnker, Rob van Glabbeek, Peter Hoefner, Annabelle McIver, Marius Portmann and Wee Lum Tan Automated analysis of AODV using UPPAAL International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 173–187, Tallinn, Estonia, March, 2012 |
2011
|
|
|
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 |
|
|
|
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 |