Keywords: process algebra, formal modelling, formal methods
Units: 12/24 units
Background
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 (http://en.wikipedia.org/wiki/IEEE_802.11s).
-
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.