Teaching

Winter 2009/10

Summer 2009

Formale Systeme, Automaten, Prozesse
Graphentheorie (Seminar)
Medizinische Bildverarbeitung (with Deserno, Kobbelt, Ney, Seidl, Spitzer)

Winter 2008/09

Summer 2008

Analyse von Algorithmen
Software-Projektpraktikum Graphalgorithmen
Medizinische Bildverarbeitung (with Deserno, Kobbelt, Ney, Seidl, Spitzer)

Winter 2007/08

Summer 2007

Datenstrukturen und Algorithmen
Medizinische Bildverarbeitung (with Kobbelt, Deserno, Ney, Seidl, Spitzer)

Former Years

Diploma/Master/Bachelor Thesis Proposals

Generisches framework für die Extraktion von finite state machines aus Quelltexten und ihre Überführung an Verifikationswerkzeuge

Motivation

Insbesondere in sicherheitskritischen eingebetteten Systemen werden sehr häufig finite state machines eingesetzt, um Systemzustände und Transitionen zwischen diesen Zuständen explizit beschreiben zu können. Diese ausdrückliche Formulierung gestattet eine saubere Modellierung des Systemverhaltens in einem weniger technischen, sondern vielmehr der Anwendungsdomäne entsprechenden Vokabular und erleichtert somit das Verständnis der Abläufe erheblich. Darüber hinaus birgt die forcierte Endlichkeit des Modells gravierende Vorteile hinsichtlich der Untersuchbarkeit z.B. im Rahmen einer formalen Verifikation. Allerdings existiert keine Einheitsimplementierung von FSMs, die allen Softwareprojekten gerecht werden könnte. Die konkrete Implementierung einer FSM wird oftmals von anwendungsspezifischen Rahmenbedingungen bestimmt. Somit existiert auch kein einheitliches Verfahren, um eine FSM einer formalen Verifikation zuzuführen.

Ziel der Arbeit

Im Rahmen dieser Diplomarbeit soll ein generisches Framework erstellt werden, mit dem FSMs aus annotierten bzw. attributierten Quelltexten extrahiert, in einem internen Format zwischengespeichert und danach in das gewünschte Zielformat (etwa Spin oder NuSMV) konvertiert werden können. Das Framework soll nicht hart auf bestimmte Sprachen beschränkt sein, sondern einfache Mechanismen für die Unterstützung weiterer Ein- und Ausgabeformate bereitstellen. Hierbei stellen sich jenseits des Entwurfs und der Programmierung von Parser und Converter noch weitere wichtige Fragen:

Wie bzw. wie weit kann garantiert werden, dass das extrahierte Modell die implementierte FSM korrekt abbildet?
Welche Einschränkungen müssen bei der FSM-Implementierung beachtet werden, welche davon lassen sich noch automatisch prüfen?
Wie lassen sich die ausgegebenen Modelle einfach für automatisierte Tests einsetzen (beispielsweise durch Integration in Testframeworks wie Rutema)?

Vorkenntnisse

C (unabdingbar) / C++ (wünschenswert)
Formale Verifikation / Model Checking
GNU/Linux/gcc

Betreuer/Gutachter

Erstgutachter: Prof. Dr. rer. nat. Peter Rossmanith, RWTH Aachen
Zweitgutachter: Prof. Dr.-Ing. Stefan Kowalewski, RWTH Aachen
Betreuer: Dr. rer. nat. Daniel Mölle, Zühlke Engineering

Referenzen

http://nusmv.irst.itc.it/ http://spinroot.com/

Making OFF work

The Owner Free File System is a real-life implementation of a brightnet, a novel approach towards privacy-aware sharing of large data volumes. Although it is technically working, there are still some issues hampering general usability and thus wide-spread adoption. Besides obvious user-interface issues, they concern aspects such as reliability, efficiency, anonymity, and scalability.

This gives rise to a number of possible theses reaching from a theoretical analysis of OFF's idea of multi-purpose encoding, to a practical evaluation of possibilities for improvement/replacement of the underlying custom-made distributed hash table, which would address all of the above aspects at once.

A comparative analysis of GNUnet and StealthNet regarding anonymity, efficiency and usability

Anonymous file sharing is a topic with many social and political implications. It has been heralded the next step from pioneering peer-to-peer applications such as Napster or Gnutella. Astonishingly, this new wave seems to be hindered by non-trivial technical problems, so that we have yet to see an anonymous file sharing network that works well enough to be accepted by the general public.

In this thesis, two systems that take very different approaches are to be analyzed in order to find an answer to the question what is the real hindrance to mass use. Ideally, the thesis should result in a clearer sight on the way to a more anonymous, efficient and usable file sharing network.

Implementing Online Codes in Bittorrent

The bittorrent protocol has become very popular for the distribution of large files. Advances in coding theory have brought forward rateless error correction codes like online codes that could potentially make multi-source downloads much more efficient.

In this thesis, the theoretical approach of a state-of-the-art error correction code like online codes is to be implemented in order to enhance the bittorrent protocol. This includes the choice of a suitable bittorrent client, development of a plug-in or similar technique to incorporate the new algorithm into the software, and performance testing. An ideal outcome would be the adoption of the new plug-in by the user base of the client which might eventually lead to adoption of the algorithm into the bittorrent protocol.

Please talk to Stefan Richter if you are interested in one of these topics or in the field of anonymous/deniable file sharing in general.

Theses in Algorithms

We have proposals for Diploma Theses in the area of Efficient Algorithms, especially Parameterized or Exact Algorithms, and related subjects. Two possible subjects are:

Finding hard instances using evolutionary algorithms
Exploiting "bad" approximation algorithms
...

Lecture Notes

Analysis of Algorithms (in German)