Studentische Arbeiten
Zertifikatsprüfung Timed Bisimulation
Type of thesis:
Bachelor-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 [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.
Task
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.
Preconditions
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.
