Trustworthy Systems

Process Algebra for Wireless Networks (AWN)

People

  • 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

2020

Abstract PDF 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
Abstract PDF Jack Drury, Peter Hoefner and Weiyou Wang
Formal models of the OSPF routing protocol
MARS2020, pp. 72–120, Dublin, Ireland, April, 2020

2019

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

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

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

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
European Symposium on Programming, 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
International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 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