Thesis Topic Details

Topic ID:
Modelling Network Routing Protocols
Peter Hofner
Research Area:
Formal Methods, System Modelling
Associated Staff
Rob van Glabbeek
Topic Details
Group Suitable:
interest in applying Formal Methods and logic-based calculi in general; previous knowledge about process algebra is appreciated, but not necessary
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 current systems often do 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 new adaptive network protocols and mechanisms for Wireless Mesh Networks 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. Close collaboration with industry partners ensures the use-inspired nature of the project.

Classical routing protocol specifications are usually written in plain English. Often this yields ambiguities, inaccuracies or even contradictions. The use of Formal Methods like process algebra avoids these problems and leads to a precise description of protocols. To compare and evaluate different protocols, we aim at a compendium of standard routing protocol specifications in a unified language.

So far we have modelled two of the standard protocols using process algebra, namely the Ad hoc On-Demand Distance Vector (AODV) and the Dynamic MANET On-demand (DYMO) routing protocol. The project's work should include the formalisation of a second standard protocol, called OSLR (url{}). After a faithful specification of OSLR has been given, the work could include the verification of basic properties or the comparison with other protocols.
An example for a basic property is packet delivery; it guarantees that a packet, which is injected into a network, is finally delivered at the destination (provided the destination can be reached).
Past Student Reports
No Reports Available. Contact the supervisor for more information.

Check out all available reports in the CSE Thesis Report Library.

NOTE: only current CSE students can login to view and select reports to download.