Process Algebra for Wireless Networks (AWN)
-
Aim: development of a process algebra that enables us to formalise, state and (dis)prove crucial properties of mesh network
routing protocols such as loop freedom and packet delivery
- Context: The development of AWN is part of Formal Methods for Wireless Networks.
-
Approach:
We propose a new process algebra AWN for wireless networks that combines
novel treatments of local broadcast, conditional unicast and data
structures. To show its applicability we modelled the Ad-hoc On-Demand Distance
Vector routing protocol (AODV and AODVv2).
We give a complete specification of this widely-used protocol.
AWN allows us to state and (dis)prove crucial properties of mesh network routing protocols such as loop freedom and packet delivery.
- Collaboration: The University of Queensland, Griffith University, INRIA
People
|
|
Activities
- Algebra of Wireless Networks: The developed process algebra combines novel treatments of data structures, conditional unicast and local broadcast, and allows formalisation of all important aspects of a routing protocol. All these features are necessary to model "real life" wireless mesh networks (WMNs). Data structures are used to store and maintain information, e.g. routing tables. The conditional unicast construct allows us to model that a node in a network sends a message to a particular neighbour, and if this fails, for example because the receiver has moved out of transmission range, error handling is initiated. Finally, the local broadcast primitive, which allows a node to send messages to all its immediate neighbours, models the wireless broadcast mechanism implemented by the physical and data link layer of wireless standards relevant for WMNs. Our formalisation assumes that any broadcast message is received by all nodes within transmission range. This abstraction enables us to interpret a failure of guaranteed message delivery as an imperfection in the protocol, rather than as a result of a chosen formalism not allowing guaranteed delivery. We are currently working on extending this process algebra with time.
- Case Study AODV: We demonstrate how our algebra can be used to formally model and reason about the Ad-Hoc On-Demand Distance Vector (AODV) routing protocol, which is one of the most relevant and widely used routing protocols in WMNs. The process algebra allows us to prove critical protocol properties like loop freedom. Our model covers all core components of AODV, but none of the optional features, and abstracts from timing issues. As a further abstraction, we assume that any broadcast message is received by all nodes within transmission range (see above).
- Proof Mechanisation: To increase the trust in our (manual) proofs and to speed-up the analysis of variants of protocols, we mechanise the proof of loop freedom in the interactive theorem prover Isabelle/HOL. Isabelle/HOL verifies the proofs to be correct. Moreover, if there is a slight change in the protocol specification (e.g. a broadcast is used instead of a groupcast) Isabelle can try to verify properties for this variant fully automatically. In case Isabelle fails, it points at the problems; hence there is no need to revisit all proofs that do not change.
Details can be found here.- On-going Work: includes the extension of AWN to include time and probability. The former allows us to model timers as they appear in AODV. By this we can analyse more aspects of wireless mesh protocols such as route lifetimes. The latter helps to model unreliable links as they appear in practice.
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 Proceedings of the 28th 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
|
|
|
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 |
|
|
|
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 |
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 |
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 |
|
|
|
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 |
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 |
|
|
|
Ansgar Fehnker, Rob van Glabbeek, Peter Hoefner, Annabelle McIver, Marius Portmann and Wee Lum Tan A process algebra for wireless mesh networks Proceedings of the 21st 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 Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 173–187, Tallinn, Estonia, March, 2012 |
Bachelor's theses
 |
|
Sarah Edenhofer Formale Spezifikation des "Dynamic MANET On-demand"-Routingalgorithmus (DYMO) Institut für Informatik, Universität Augsburg, Germany, March, 2012 |