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: Bachelor-Thesis, 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 [TChecker] ermöglichen Simulation und Analyse modellierter Systeme und tragen so wesentlich zur Ausfallsicherheit des Endproduktes bei.

Mithilfe von Timed Bisimulation lässt sich prüfen, ob zwei Timed Automata sich identisch verhalten. Hierdurch ist es beispielsweise möglich, die Modellierung einer Implementierung mit der Modellierung einer Spezifikation zu vergleichen und Fehler in der Implementierung zu finden.

Am Fachgebiet Echtzeitsysteme wurde ein neuartiger Algorithmus zum Überprüfen von Timed Bisimulation entwickelt und implementiert. Um den Nutzer restlos von der Korrektheit des Ergebnisses zu überzeugen, ist jedoch eine Zertifikatsanzeige notwendig, welche übersichtlich und einfach zu bedienen ist. Im Falle einer positiven Prüfung enthält das Zertifikat die gefunden Zuordnungen zwischen den Zuständen des TA, während im Falle einer negativen Prüfung der Unterschied hinterlegt wird.

Aufgabenstellung

Es soll ein Dateiformat erarbeitet werden, in welchem unsere Implementierung das Zertifikat speichert. Im Anschluss soll ein bestehendes grafisches Tool [https://github.com/Echtzeitsysteme/timed-automata-analysis-frontend] erweitert werden, sodass das Zertifikat eingelesen und mithilfe einer Spielsemantik vom Nutzer geprüft werden kann.

Die Userinteraktion soll ähnlich wie bei dem Tool [Caal] sein.

Voraussetzungen

Sehr (!) gute Kenntnisse in Typescript und React.

C++ wünschenswert.

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.

Zurück zur Übersicht

Zu den abgeschlossenen Arbeiten