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
|
|
- 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
|
 |
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 |
Contact
Peter Höfner, peter.hoefner <at> data61.csiro.au