Abgeschlossene Arbeiten

Studentische Arbeiten

Bisimulations-Analyse von echtzeitkritischen Software-Produktlinien

Typ der Arbeit: Master-Thesis
Bearbeitungsstand: Abgeschlossene Arbeiten
Arbeit abgeschlossen am: 11.06.2020
Betreuer*in: M.Sc. Lars Luthmann
Student*in: Isabelle Bacher

Zurück zur Übersicht

Motivation

Timed Automata (TA) bieten mit ihren diskreten Zuständen und ihrem kontinuierlichen Zeitverhalten eine Möglichkeit zur Abbildung echtzeitkritischer Software-Systeme. Vor allem in der Phase der Wartung einer Software während der Software-Entwicklung ist die Überprüfung auf gleiches Verhalten zwischen dieser und der Spezifikation wichtig, um eventuell fehlerhafte Konfigurationen durch neu hinzugefügte Funktionen feststellen zu können. Während die Äquivalenz von Traces nicht entscheidbar ist, kann jedoch mittels der Timed Bisimulation eine entscheidbare Aussage über gleiches Verhalten getroffen werden. Eine effektive Überprüfung auf Bisimilarität von Zone-History Graphen, die eine effiziente Darstellung der TA-Semantiken bieten, ist bereits möglich. Jedoch wird dabei nur deterministisches Verhalten unterstützt. Die Umsetzung von nicht-deterministischem Verhalten und internen Transitionen fehlt noch. Zudem besitzen TA nur eine beschränkte Ausdruckskraft, sodass die Variabilität von Software- Produktlinien nicht abgebildet werden kann. In dieser Thesis erfolgt deshalb zunächst die Erweiterung um nicht-deterministisches Verhalten und die Behandlung von internen Transitionen. Anschließend werden TA mit der Einführung von Parametern in den Clock Constraints und der daraus resultierenden Erweiterung der TA zu Parametric Timed Automata (PTA) um mehr Variabilität durch variable Grenzen von Intervallen ergänzt. Die Timed Bisimulation wird deshalb zur Parametric Timed Bisimulation erweitert. Da viele Eigenschaften für TA entscheidbar, jedoch für PTA nicht entscheidbar sind, wird mithilfe der Lower-bound/Upper-bound Parametric Timed Automata (L/U-PTA), einer Subklasse der PTA, eine Approximation der PTA-Semantiken auf TA-Semantiken durchgeführt.

Zurück zur Übersicht