Skip to main content

Process Algebra for Wireless Networks

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

Current

Past

  • Emile Bres
  • Matthias Daum
  • Tran Ngoc Ma

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

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

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

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

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 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

Bachelor's theses

Abstract PDF Sarah Edenhofer
Formale Spezifikation des "Dynamic MANET On-demand"-Routingalgorithmus (DYMO)
Institut für Informatik, Universität Augsburg, Germany, March, 2012

Contact

Peter Höfner, peter.hoefner <at> data61.csiro.au
Served by Apache on Linux on seL4.