Modelling, Analysing and Verifying Routing Protocols

Keywords: process algebra, formal modelling, formal methods
Units: 12/24 units


Wireless Mesh Networks (WMNs) are a promising technology that is currently being used in a wide range of application areas, including Public Safety, Transportation, Mining, etc. Typically, these networks do not have a central component (router), but each node in the network acts as an independent router, regardless of whether it is connected to another node or not. They allow reconfiguration around broken or blocked paths by ``hopping’’ from node to node until the destination is reached. Unfortunately, the performance of current systems often does not live up to the expectations of end users in terms of performance and reliability, as well as ease of deployment and management.

We explore and develop adaptive network protocols and mechanisms for WMNs that can overcome the major performance and reliability limitations of current systems. To support the development of these new protocols, the project also aims at new Formal Methods based techniques, which can provide powerful new tools for the design and evaluation of protocols and can provide critical assurance about protocol correctness and performance.

Research Questions and Tasks

Routing protocol specifications are usually written in plain English. Often this yields ambiguities, inaccuracies or even contradictions. Moreover no formal guarantees can be given based on such a description. The use of Formal Methods such as process algebra avoids these problems, leading not only to a precise description of protocols, but also allowing formal reasoning. The project’s work will be in this area; it can include

  • Modelling Routing Protocols

    So far we have modelled two of the standard protocols using process algebra, namely AODV and OLSR, as well as a draft successor protocol of AODV that is currently being discussed by the Internet Engineering Task Force (IETF). The project’s work could include the formalisation of a second standard protocol such as HWMP (

  • Analysing and Verifying Routing Protocols

    Based on a faithful specification that has been given, the work could include the verification of basic properties of the routing protocol: packet delivery for example guarantees that a packet, which is injected into a network, is finally delivered at the destination (if the destination can be reached).

  • Tool Support

    The generation of tools for (semi)automatic reasoning is of high interest. For our work we have used the interactive theorem prover Isabelle and the model checker Uppaal. So far, the use of these tools includes manual work. The project’s work could also aim at more automation: this can be automatic translation software from a process algebra language to a model description for Uppaal; or the development of proof-tactics for Isabelle.

Requirements: The concrete requirements depend on the chosen topic and the applicant’s interests and strengths. An interest in formal methods is a must, though.

You are on Aboriginal land.

The Australian National University acknowledges, celebrates and pays our respects to the Ngunnawal and Ngambri people of the Canberra region and to all First Nations Australians on whose traditional lands we meet and work, and whose cultures are among the oldest continuing cultures in human history.

arrow-left bars search times arrow-up