Provably accurate verdictors : foundations and applications

Abstract

This thesis introduces provably accurate verdictors, systems designed to provide provably accurate answers to pressing operational questions about a system by observing its behavior. For instance, verdictors can detect faults in aircraft sensors or incorrect configurations in manufacturing equipment at runtime. Such information is critical for ensuring system safety and availability, enabling informed safeguarding and timely interventions. Adopting a model-based methodology, this thesis leverages formal models as the ground truth for a system's behavior and properties. A comprehensive theoretical framework is established, providing a precise formal characterization for what it means to provide provably accurate answers. Building on this framework, the thesis develops generic algorithms for implementing and synthesizing provably accurate verdictors in both discrete and continuous-time settings, focusing on robustness against observational imperfections such as losses and delays. The versatility and effectiveness of these algorithms is demonstrated across diverse applications, including runtime verification and fault diagnosis. Additionally, the thesis introduces variability-aware monitoring, addressing significant challenges in monitoring configurable systems with configurable verdictors. With Momba, a new state-of-the-art tool for formal modeling is presented. Using Momba, the theoretical contributions of the thesis are implemented, validated, and empirically evaluated.

Diese Dissertation stellt nachweisbar akkurate Verdiktoren vor, Systeme, die durch die Beobachtung eines Systems akkurate Antworten auf betriebskritische Fragen liefern. So können zur Laufzeit Fehler in Flugzeugsensoren oder falsche Konfigurationen von Produktionsanlagen erkannt werden. Solche Informationen sind entscheidend für die Systemsicherheit und -verfügbarkeit, da sie fundierte Schutzmaßnahmen und rechtzeitige Eingriffe ermöglichen. Diese Arbeit verfolgt einen modellbasierten Ansatz, bei dem formale Modelle als Referenz für das Systemverhalten dienen. Es wird ein theoretisches Rahmenwerk entwickelt, das präzise definiert was es bedeutet, nachweisbar akkurate Antworten zu liefern. Darauf aufbauend werden generische Algorithmen zur Implementierung und Synthese von nachweisbar akkuraten Verdiktoren für diskrete und kontinuierliche Zeitmodelle entwickelt, wobei der Schwerpunkt auf Robustheit gegenüber Beobachtungsimperfektionen, z.B., Verzögerungen und Verlusten, liegt. Die Vielseitigkeit und Effektivität dieser Algorithmen wird in verschiedenen Anwendungsbereichen wie Laufzeitverifikation und Fehlerdiagnose demonstriert. Zudem wird variabilitätsgewahres Überwachen eingeführt, um konfigurierbare Systeme mithilfe von konfigurierbaren Verdiktoren zu überwachen. Mit Momba wird ein modernes Werkzeug für formales Modellieren vorgestellt. Die entwickelten Ansätze werden in Momba implementiert und durch empirische Studien evaluiert sowie validiert.