[Back]


Doctor's Theses (authored and supervised):

T. Reinbacher:
"Analysis of Embedded Real-Time Systems at Runtime";
Supervisor, Reviewer: A. Steininger, J. Schumann, S. Kowalewski; Institut für Technische Informatik, 2013.



English abstract:
The capabilities to design embedded real-time systems have outpaced the capabilities to
verify these systems. With this imbalance comes the immediate need for solutions to deal
with situations where bugs, unnoticed during verification, manifest themselves at runtime.
To tackle this problem, this thesis develops a novel framework to perform analysis of
embedded real-time systems at runtime. The framework arises from the idea of combining
a status-assessment component with a health-estimation component and is intended to
be attached to existing embedded real-time systems as a self-contained hardware unit.
The status-assessment component of our framework builds on runtime verification
and aims at a fine-grained technique to assess the status of the analyzed system with
respect to a specification written in different flavors of temporal logic. Our framework
minimizes interference with the analyzed system by collecting updates about the state of
the system through wiretapping of existing communication interfaces. These updates are
then processed by a set of novel observer algorithms that assess the system´s status. A
status assessment is composed out of the results of the satisfiability checks for each item
of the specification, thus, can be understood as a filtered snapshot of the current state of
the analyzed system. The observer algorithms we present are designed with the intention
to map them into highly parallel, reconfigurable hardware units. We provide formal
correctness proofs for all the presented algorithms, analyze their time and space complexity,
and discuss their efficient implementation in hardware. The obtained results are promising
with respect to a self-contained, responsive, and unobtrusive status-assessment component.
The health-estimation component of our framework builds on Bayesian inference and
aims at providing a continuous estimation of the analyzed system´s health with respect to
a given health model. Input to this health model is the system´s status, computed by the
status-assessment component. We compile health models, specified as Bayesian networks,
into arithmetic circuits and lift an inference algorithm to a highly parallel setting by
exploiting structural properties of arithmetic circuits. This allows us to design a hardware
architecture that natively supports inference of posterior marginals on health models,
supporting our aim of a self-contained, responsive health-estimation component.
We demonstrate the benefits of our runtime analysis framework by analyzing actual
flight data from an unmanned NASA aircraft. We outline a workflow to integrate
our approach into existing development cycles. Following this workflow, we derive a
specification to state time-bounded properties and a health model for the altimeter
subsystems of the aircraft. In a post-flight analysis, an instance of our framework
on a Field Programmable Gate Array (FPGA) successfully detected, in real-time, an
unexpected drop in one of the altimeter readings and correctly identified an outage of the
laser altimeter as the root cause. These findings matched diagnosis by test engineers.

German abstract:
Effiziente moderne Tools erlauben es hoch komplexe eingebettete Systeme zu bauen, deren
Verifikation dann jedoch oft die Möglichkeiten verfügbarer Methoden übersteigt. Die
Gefahr, dass Bugs während der Testphase unentdeckt bleiben, wird folglich größer; dem
entsprechend werden Ansätze benötigt, um geeignet mit Bugs während der operativen
Phase eines Systems umzugehen. Eben dieser Problematik widmet sich die vorliegende
Dissertation. Es wird ein auf Hardware basierender Ansatz für die automatisierte Analyse
eingebetteter Echtzeitsysteme während der Laufzeit vorgestellt, der in zwei Schritten
arbeitet, nämlich (i) der Erfassung des Systemstatus mittels Runtime Verification sowie
(ii) der Diagnose der Ursachen von Fehlfunktionen mittels Bayesscher Statistik.
Runtime Verification ist eine inzwischen etablierte Technik für die Überprüfung
der Korrektheit der Abläufe in einem System gegenüber einer formalen Spezifikation.
Bestehende Ansätze hierfür bedingen meist die Instrumentierung der Software des zu
prüfenden Systems. In der Praxis ist dies jedoch schwer zu bewerkstelligen, da eingebettete
Systeme oft aus einer Vielzahl von Komponenten unterschiedlichen Ursprungs bestehen,
von denen manche zudem bereits zertifiziert sind und daher nicht modifiziert werden
dürfen. Anstelle einer Instrumentierung baut der hier vorgestellte Ansatz auf das passive
Abgreifen der relevanten Informationen an bereits vorhandenen Kommunikationskanälen.
Zur Statuserfassung werden neuartige Algorithmen entwickelt, welche die so abgegriffenen
Signalpegel gegenüber Spezifikationen in verschiedenen temporalen Logiken auswerten.
Damit dies effizient zur Laufzeit möglich ist, wird dabei auf deren Implementierbarkeit in
Hardware spezieller Wert gelegt. Die Korrektheit der Algorithmen wird bewiesen, und
die Untersuchung der Zeit- und Speicherkomplexität bestätigt die Anwendbarkeit der
Algorithmen für eine minimal-invasive Harwarekomponente zur Statuserfassung.
Die vorgeschlagene Diagnosekomponente verarbeitet die Resultate der Statuserfassung
und nimmt hierfür Anleihe an der Theorie der Bayesschen Statistik. Ein Fehlermodell wird
als Bayessches Netz spezifiziert und dieses dann in einen Graphen übersetzt. Damit derartige
Fehlermodelle von einer hoch-parallelen Hardwareeinheit zur Laufzeit ausgewertet
werden können, wird ein bestehender Algorithmus geeignet parallelisiert.
Die industrielle Anwendbarkeit dieses neuen Ansatzes wird anhand der Analyse realer
Flugdaten eines unbemannten Luftfahrzeugs der NASA nachgewiesen. Für diese Beispielanwendung
wird erst ein Workflow zur Integration des Ansatzes in bestehende Entwicklungsprozesse
vorgestellt. Darauf aufbauend wird exemplarisch eine temporale Spezifikation
erstellt um zeitbehaftete Eigenschaften des Luftfahrzeugs zu überprüfen, sowie ein Fehlermodell
entwickelt, welches die Komponenten zur Höhenmessung abdeckt. Der vorgestellte
Ansatz erkennt, in Echtzeit und automatisch, einen Fehler in der Höhenmessung und
identifiziert korrekt eine Fehlfunktion des Laserhöhenmessers als Ursache.


Related Projects:
Project Head Andreas Steininger:
Framework für CounterExample Validierung und Testfallgenerierung für die Verifikation von eingebetteter Software


Created from the Publication Database of the Vienna University of Technology.