Reinbacher, T. (2013). Analysis of embedded real-time systems at runtime [Dissertation, Technische Universität Wien]. reposiTUm. http://hdl.handle.net/20.500.12708/159685
Verifikation zur Laufzeit; Observer Algorithmen; Eingebettete Echtzeitsysteme; System Health Management
de
Runtime Verification; Observer Algorithms; Embedded Real-Time Systems; System Health Management
en
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. Dieser Problematik widmet sich diese 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: Erfassung des Systemstatus mittels Runtime-Verification und Diagnose der Ursachen von Fehlfunktionen mittels Bayesscher-Statistik. Zur Statuserfassung werden neuartige Algorithmen entwickelt, welche das Verhalten des Systems 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. 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 Anleihe an der Theorie der Bayesschen Statistik. Fehlermodelle werden als Bayessches Netz spezifiziert und in Graphen übersetzt. Damit diese von einer hoch-parallelen Hardwareeinheit zur Laufzeit ausgewertet werden können, wird ein bestehender Algorithmus geeignet parallelisiert. Die industrielle Anwendbarkeit dieses Ansatzes wird anhand der Analyse realer Flugdaten eines unbemannten Luftfahrzeugs der NASA nachgewiesen. Eine temporale Spezifikation wird erstellt um zeitbehaftete Eigenschaften des Luftfahrzeugs zu überprüfen, sowie ein Fehlermodell entwickelt, welches die Komponenten zur Höhenmessung abdeckt. Der Ansatz erkennt, in Echtzeit und automatisch, einen Fehler und identifiziert korrekterweise eine Fehlfunktion des Laserhöhenmessers als Ursache.
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 combines 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. A status assessment is composed out of the results of the satisfiability checks for each item of the temporal-logic based specification. We present efficient observer algorithms for these specifications, provide formal correctness proofs, analyze their time and space complexity, and discuss their efficient implementation in hardware. 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. 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 an efficient hardware architecture. We demonstrate the benefits of our framework by analyzing flight data from an unmanned NASA aircraft. In a post-flight analysis, an instance of our framework 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.