Folgende Materialien helfen beim Erstellen von wissenschaftlichen Arbeiten:

• Vorlage für Studien-, Bachelor und Masterarbeiten am FG Echtzeitsysteme [Github]
• Vorlage für Präsentationen am FG Echtzeitsysteme [Github]

Typ der Arbeit: Master-Thesis
Bearbeitungsstand: Offene Arbeiten
Betreuer*in: M.Sc. Alexander Lieb

Zurück zur Übersicht

Motivation

Timed Automata sind ein weit verbreiteter Formalismus zur Modellierung von Echtzeitsystemen. Tools wie [Uppaal] ermöglichen Simulation und Analyse modellierter Systeme und tragen so wesentlich zur Ausfallsicherheit des Endproduktes bei. [Hier] finden Sie eine (nicht abgeschlossene) Liste an beispielhaften Case Studies zu diesem Thema.

Analog zu Programmiercode kann auch eine solche Modellierung statische Anomalien, beispielsweise unnötige Transitionen, aufweisen. Diese stellen mögliche Modellierungsfehler dar, auf die der Anwender hingewiesen werden sollte. Des Weiteren verbessert die Ausbesserung von Anomalien möglicherweise die Performanz der Analysetools, sodass die Betrachtung noch komplexerer Systeme möglich wird.

Aufgabenstellung

Auf Basis einer umfassenden Literaturrecherche und Ideen des Studierenden soll ein Tool zur Erkennung statischer Anomalien für Timed Automata erstellt werden. Die Konzepte der einzelnen Erkennungsfeatures sollen mathematisch beweisbar sein. Je nach Aufwand sind weitere Ausbaustufen denkbar, beispielsweise die Erkennung zu starker/schwacher Teilbedingungen an Transitionen oder die Erstellung von Verbesserungsvorschlägen für den Anwender. Eigene Ideen sind hierbei erwünscht.

Die Thesis kann sowohl auf Deutsch als auch auf Englisch geschrieben werden.

Um für Sie ein passendes Thema in diesem Bereich zu finden, setzen Sie sich bitte mit dem Betreuer dieser Arbeit in Verbindung.

Voraussetzungen

Vorlesung Software Engineering - Wartung und Qualitätssicherung (oder vergleichbar).

Formale Methoden im Softwareentwurf (oder vergleichbar).

Vorlesung Echtzeitsysteme (wünschenswert, aber nicht zwingend erforderlich).

Stark ausgeprägtes Interesse an beweisbarer Algorithmik.

Grundkenntnisse und Interesse an Aufgabenstellungen aus dem Bereich der Theoretischen Informatik.

Gute Java-Kenntnisse.

Falls Sie sich grundsätzlich in Timed Automata einlesen möchten, können Sie

Timed Automata: Semantics, Algorithms and Tools, Johan Bengtsson and Wang Yi. In Lecture Notes on Concurrency and Petri Nets. W. Reisig and G. Rozenberg (eds.), LNCS 3098, Springer-Verlag, 2004.

als Ausgangspunkt verwenden.

Zurück zur Übersicht

Zu den abgeschlossenen Arbeiten