Abstract

Background

Formal analysis is currently hardly applied during the development of routing protocols. Some issues with protocols are only discovered after standardization and implementation on a large scale. The Border Gateway Protocol (BGP), for example establishes routes between internet service providers. However, BGP routers can cycle through all possible routes, so the network may not converge. Its extension with “route flap damping” appeared to have negative side-effects. Another example is the popular Ad-hoc On-Demand Distance Vector (AODV) protocol for WMNs (Wireless Mesh Networks) and MANETs (Mobile Ad-hoc Networks). This does not even satisfy loop-freedom and eventual packet delivery.

Formal analysis of routing protocols could discover such problems during development. It requires wireless protocols to be formally specified – improving on current ambiguous and incomplete specifications. The informal specification of the AODV protocol was open to 5184 different interpretations! It would be useful to develop tools that make formal specification and analysis of routing protocols more accessible to developers.

In 2012, AWN (Algebra for Wireless Networks) was proposed. Its purpose is to specify WMN and MANET protocols unambiguously and validate them exhaustively. The ultimate goal is to reduce development and maintenance time and to increase reliability and performance.

This thesis

This MSc thesis describes an approach to automatically model and verify AWN specifications with existing model checking toolsets, by translating AWN to model checkers’ input. This translation allows the verification of properties of a network. A plain-text input language for AWN was developed, including data expressions. This made it possible to implement a development environment for AWN in Eclipse, providing syntax highlighting, code completion, refactoring facilities, and more. The environment also serves as a front end for a translation to mCRL2, a generic process algebra with a verification toolset. This translation was implemented as a module in a translation framework – more translations can easily be added in the future.

The mathematical underpinning of the translation preserves essential properties of the respective operational semantics. Due to the semantic gap, a new form of bisimulation had to be invented, bridging AWN and mCRL2 models. This thesis provides a full mathematical proof that the transformation preserves the semantics for all AWN models.

The thesis formed the basis of a paper published at the International Conference on Integrated Formal Methods: Rob van Glabbeek, Peter Höfner, Djurre van der Wal: Analysing AWN-Specifications Using mCRL2. IFM 2018.

Artifact and paper are online at: http://www.hoefner-online.de/home/conferences/ifm18/

References

1. IFM 2018 (Digital version available here)

Additional Resources

1. MSc thesis