Studentische Arbeiten
Reverse Engineering von Parametric Timed Automata aus konfigurierbarem C-Code
Typ der Arbeit:
Master-Thesis
Bearbeitungsstand: Abgeschlossene Arbeiten
Arbeit abgeschlossen am: 09.05.2018
Betreuer*in: Dr.-Ing. Lars Luthmann
Motivation
Während der Entwicklung und Nutzung vieler hardwarenaher Softwaresysteme ist es für den sicheren Betrieb wichtig, dass feste Zeitbedingungen eingehalten werden. Timed Automata sind ein bewährtes Konzept, um die Analyse und Verifikation dieser Zeitbe- dingungen durchzuführen. Mit der Entwicklung von Softwaresystemen als Software- Produktlinien vergrößert sich die Menge zu überprüfender Software. Das Konzept der Timed Automata wird durch Configurable Parametric Timed Automata (CoPTA), um Features und Parameter erweitert, die es ermöglichen Software-Produktlinien als Timed Automata zu modellieren.
Ein Problem in der industriellen Praxis ist es, dass Software, deren Zeitbedingungen überprüft werden soll, ausschließlich als C-Code vorliegt, während die Analyse CoPTA- Modelle als Abstraktion benötigt. Ziel dieser Arbeit ist es deshalb, ein Reverse-Engineering der benötigten CoPTA-Modelle aus konfigurierbarem C-Code zu automatisieren.
Diese Arbeit stellt Konzepte vor, wie mithilfe der Zwischendarstellung von Programm- code als Kontrollfluss-Automaten eine Generierung von CoPTAs stattfinden kann und wie diese Automaten, mithilfe von Tools für die Analyse von Ausführungszeiten, um Zeitbedingungen erweitert werden können. Die abschließende Evaluation des Tools wertet dessen Funktionalität anhand der Software-Produktlinienimplementierung eines Open-Source-Projektes aus.
