Studentische Arbeiten
Statische Analyse von Timed Automata
Type of thesis:
Master-Thesis
State: Offene Arbeiten
Tutor: M.Sc. Alexander Lieb
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.
Task
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.
Preconditions
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 C++ Kentnisse.
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.
(https://www.seas.upenn.edu/~lee/09cis480/papers/by-lncs04.pdf) als Ausgangspunkt verwenden.