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 Adhoc OnDemand Distance
Vector routing protocol (AODV and AODVv2).
We give a complete specification of this widelyused 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 AdHoc OnDemand 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 speedup 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. Ongoing 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
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
2016
2015
Peter Hoefner Using process algebra to design better protocols (abstract) Forum “MathforIndustry” 2015, pp. 31–33, Fukuoka, Japan, October, 2015 
2014
2013
2012
Bachelor's theses
Sarah Edenhofer Formale Spezifikation des "Dynamic MANET Ondemand"Routingalgorithmus (DYMO) Institut für Informatik, Universität Augsburg, Germany, March, 2012 