Project Offers

This page lists a couple of projects we are offering at the moment. However, projects are not limited to the listed projects. In case you want to write your thesis with us or in case you are interested in an internship, feel free to contact us directly.

PhDs

We are always willing to superwise (good) PhD students. Please contact us directly in case you are interested in doing a Phd in the wide area of formal modelling, reasoning and analysis. In particular we offer PhD topics in the area of process algebra, Kleene algebra, wireless mesh networks, software defined networks and expressivness.
 
Go Up

Master's/Bachelor's/Honour's Theses

Please contact us in case you want to write your thesis under our supervision. If you are interested in formal reasoning, formal modelling or verification and you do not find a topic in the list below, please contact us—we might have more topics available.
 
  1. Timed AWN — A Timed Process Algebra for Wireless Mesh Networks (Msc/Hon)

    Wireless Mesh Networks (WMNs) have recently gained considerable popularity and are increasingly deployed in a wide range of application scenarios, including emergency response communication, intelligent transportation systems, mining, video surveillance, etc. WMNs are essentially self-organising wireless ad-hoc networks that can provide broadband communication without relying on a wired backhaul infrastructure.
    Recently, a process algebra for wireless mesh networks (AWN) has been developed. It combines novel treatments of data structures, conditional unicast and local broadcast, and allows formalisation of all important aspects of a routing protocol. (In WMNs, a routing protocol is used to establish and maintain network connectivity through paths between source and destination node pairs.) All these features are necessary to model "real life" WMNs; for example it has been demonstrated that AWN can be used to formally model and reason about the Ad-Hoc On-Demand Distance Vector (AODV) routing protocol.
    However, a feature missing so far is time. This does not matter when analysing reactive protocols, such as AODV; but time is required and necessary when modelling other types of protocols, such as link state protocols. Aim of the project is to extend AWN by time. The first outcome should be a timed version of AWN, including suitable primitives for timing and structural operational semantics. To demonstrate the use of the new algebra, it should be used to formally model and reason about a simple protocol, for example B.A.T.M.A.N. (the second outcome).

    Contact: R.J. van Glabbeek

  2. Modelling Routing Protocols (Msc/Bsc/Hon)

    Wireless Mesh Networks (WMNs) are a promising technology that is currently being used in a wide range of application areas, including Public Safety, 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. In WMNs, a routing protocol is used to establish and maintain network connectivity through paths between source and destination node pairs. As a consequence, the routing protocol is one of the key factors determining the performance and reliability of WMNs. Specifications for routing protocols are usually written in plain English. This often 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 third standard protocol, called OLSR(v2) (http://en.wikipedia.org/wiki/Optimized_Link_State_Routing_Protocol). To achieve this formalisation, it is also necessary to introduce suitable notion for timing primitives into the description language. After a faithful specification of OLSR has been given, the work could include the verification of basic properties. An example for such a 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).

    Contact: P. Höfner

  3. What's a good routing protocol? — Measurements for Comparing Routing Protocols (Msc/Bsc/Hon)

    Routing protocols specify how routers communicate with each other, disseminates information to select routes between any two nodes on a network and provides the ground for sending data (packets) through a network. They find applications in all types of (communication) networks, such as metropolitan area networks (MAN), local area networks (LAN), virtual private networks (VPN) or wireless mesh networks (WMN). Due to the diversity in applications dozens of (classes of) different protocols have been developed. Often there are several protocols for the same type of networks. In the case of WMNs there are for example reactive protocols, such as AODV or DYMO, and link-state protocols, such as B.A.T.M.A.N. or OLSR.
    All protocols have been implemented and deployed (in test-beds and in reality). A question which remains is, which protocol should be used in certain circumstances: Is AODV better than OLSR, if there is only few network traffic? Should B.A.T.M.A.N be used in highly-connected networks only? ... To answer these questions systematically, network topologies have to been classified, using different metrics.
    Aim of the project is to define properties that can be used as measurements for routing protocols. An example can be the amount of control messages sent. To show the usefulness of the measurements, different protocols such as AODV, DYMO and B.A.T.M.A.N. should be compared.

    Contact: P. Höfner

  4. Different Classes of Topologies and Their Effect on Routing Protocols (Msc/Bsc/Hon)

    Routing protocols specify how routers communicate with each other, disseminates information to select routes between any two nodes on a network and provides the ground for sending data (packets) through a network. They find applications in all types of (communication) networks, such as metropolitan area networks (MAN), local area networks (LAN), virtual private networks (VPN) or wireless mesh networks (WMN). Due to the diversity in applications dozens of (classes of) different protocols have been developed. Often there are several protocols for the same type of networks. In the case of WMNs there are for example reactive protocols, such as AODV or DYMO, and link-state protocols, such as B.A.T.M.A.N. or OLSR.
    All protocols have been implemented and deployed (in test-beds and in reality). By this it has been shown that protocols behave differently on different topologies.
    For example in a star topology the centre has to forward (nearly) all messages and might be too busy to react in an appropriate time for some requests.
    The main part of the project should be the creation of a topology zoo and its classification. Classification metrics used should include the average connectivity of a node; the network diameter; the density of the topology; and the beta index. After the classification metrics have been chosen; sample topologies for each category should be generated. While generating topologies it should also be determined if some topologies are members of different classes.
    The second part of the project should demonstrate the usefulness of the classification. To achieve this, one particular routing protocol, e.g. AODV, should be analysed. In particular, it should be determined if the routing protocol behaves differently on different classes of topologies.

    Contact: P. Höfner

Go Up

DAAD Rise (Research Internship in Science and Engineering)

DAAD-funded scholarships. Students in the early stages of their studies who have the ambition to work abroad and gain hands-on research experience in their fields will be matched with researchers worldwide. DAAD will support these short-term summer internships by awarding scholarships to successful applicants to help cover part of the living and travel costs.
(daad.de/rise-weltweit/en/)
 
  1. Model Checking Tool Suite for Protocol Development

    Our techniques used for modelling, analysing and verifying routing protocols for Wireless Mesh Networks (WMNs) are based on a simple programming language, which offers expressions for (arbitrary) data structures and basic primitives for WMNs, such as broadcast and unicast. The intention is to use this language right from the beginning when designing protocols; but this can only be achieved if tools support the development. During Rise 2012 and 2013 a translator from the specification language to the input language of the model checker Uppaal has been developed. During Rise 2013 a text-editor front-end for the specification language has been developed as well. The first task of the project is the combination of the two projects; by this a tool suite is created which can be used to design new protocols and which immediately offers model checking support. The second aim is to extend the tool suite by a set of standard tests which can be used to automatically analyse protocols during development and to offer on-the-fly feedback to the user.

    Further Details: pdf
    Deadline: Jan 12, 2014 (Application via DAAD)
    Contact: P. Höfner

  2. Modelling Network Routing Protocols

    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 OLSR (http://en.wikipedia.org/wiki/Optimized_Link_State_Routing_Protocol). After a faithful specification of OLSR 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).

    Further Details: pdf
    Deadline: Jan 12, 2014 (Application via DAAD)
    Contact: P. Höfner

  3. Controlling and Designing Software Defined Networks

    Software Defined Networks (SDNs) allow network administrators to have programmable central control of network traffic via a controller without requiring physical access to the network's switches. A configuration of an SDN can create a logical network control where hardware is physically decoupled from the data forwarded, i.e. network switches follow the rules given by the controller and only forward packets by the given rules.
    Up to date network configuration often requires the configuration of each and every router separately, which of course yields a huge effort. For SDNs, however, there are prototypic languages which can manage the configuration of routers automatically (e.g. NetCore). Aim of the project is to analyse the capabilities of such a language and use the language to formalise contemporary network routing.

    Further Details: pdf
    Deadline: Jan 12, 2014 (Application via DAAD)
    Contact: P. Höfner

Go Up
Last update: Dec 15, 2016