Specification mining for cyber-physical systems

Abstract

Cyber-Physical Systems (CPS) sind weit verbreitete, komplexe Systeme, die rechnergestützte und physikalische Komponenten integrieren und so eine kontinuierliche Interaktion mit der realen Umgebung ermöglichen. In den letzten Jahren hat die Integration von Machine-Learning-Komponenten zur Entwicklung lernfähiger CPS geführt, die autonom agieren können. CPS finden Anwendung in verschiedenen Bereichen, darunter autonomes Fahren, medizinische Geräte, Smart Cities, Robotersysteme und intelligente Stromnetze.Mit zunehmender Komplexität der CPS wird die Sicherstellung ihrer Vertrauenswürdigkeit immer herausfordernder, bleibt jedoch insbesondere in sicherheitskritischen Bereichen essenziell. Formale Spezifikationen sind entscheidend, um Anforderungen an das Systemverhalten eindeutig zu formulieren. Ihre mathematische Struktur ermöglicht zudem die Automatisierung von Laufzeitverifikationsverfahren – wie Überwachung, Laufzeitdurchsetzung und Falsifikation –, die eine skalierbare Überprüfung von Systemausführungen bieten. Trotz ihrer Bedeutung sind formale Spezifikationen oft nicht verfügbar, da ihre manuelle Definition aufgrund der Systemkomplexität, unvorhersehbarer Umgebungen und der großen Menge gesammelter Daten schwierig ist. Das Forschungsfeld des Specification Mining befasst sich mit der automatischen Ableitung von Systemeigenschaften durch die Analyse von Systemausführungen und deren Interaktionen mit der Umgebung.In dieser Arbeit adressieren wir mehrere Forschungslücken im Bereich des Specification Mining für CPS. Insbesondere konzentrieren wir uns auf Signal Temporal Logic (STL), ein weit verbreitetes formales Mittel zur verständlichen Darstellung zeitlicher Eigenschaften von CPS. Wir präsentieren eine Methode zur automatischen Generierung von STL-Spezifikationen, die Sicherheitsverletzungen frühzeitig anhand von ausschließlich beobachtbaren Systemvariablen vorhersagen kann. Darüber hinaus entwickeln wir eine neuartige Technik zur Bestimmung optimaler Parameterwerte für STL-Formeln, um eine Multi-Klassen-Klassifikation von Systemausführungen durchzuführen. Anschließend stellen wir die erste Methode zur Extraktion von STL-Hyperproperties vor, welche die Ausdruckskraft von Eigenschaften erweitert, indem sie Zusammenhänge zwischen mehreren Systemausführungen erfasst. Schließlich untersuchen wir die Form von Systemausführungen und extrahieren formale Spezifikationen zur Charakterisierung ihrer geometrischen Muster, die insbesondere für die Analyse von Zeitreihendaten mit wiederkehrenden Mustern nützlich sind. Wir bewerten die Leistung jeder vorgeschlagenen Methode anhand mehrerer Fallstudien sowie die Interpretierbarkeit der Formeln.

Cyber-Physical Systems (CPS) are widely used complex systems that integrate computational and physical components, enabling continuous interaction with the real-world environment. In recent years, the integration of Machine Learning components has given rise to learning-enabled CPS, allowing them to operate autonomously. CPS applications span various domains, including self-driving vehicles, medical devices, smart cities, robotic systems, and smart grids. As CPS grow in complexity, ensuring their trustworthiness has become increasingly challenging but remains essential for their adoption, especially in safety-critical domains. In this context, formal specifications are crucial for expressing requirements on system behavior in a precise and unambiguous way. Additionally, their mathematical structure enables the automation of runtime verification techniques –such as monitoring, runtime enforcement, and falsification– which provide rigorous yet scalable methods for verifying system executions. Despite their importance, formal specifications are often unavailable because manually defining them is challenging due to system complexity and unpredictable environments. Specification mining addresses this issue as it is the research field dedicated to automatically inferring system properties from its executions and interactions with the environment. In this thesis, we address several research gaps in specification mining for CPS. Specifically, we focus on Signal Temporal Logic (STL), a popular formalism for expressing temporal properties of CPS in a rigorous yet human-understandable manner, and its extensions. We introduce a method for learning STL specifications that can predict safety violations in advance based only on variables that are observable by the system, thus allowing the autonomous assessment of its safety at runtime. Moreover, we propose a new technique for learning parameter values for STL formulas to perform multi-class classification of system executions, which is essential, for instance, in recognizing different system failures simultaneously. We then develop the first method for mining STL hyperproperties, which enhance the expressiveness of properties by capturing relationships across multiple system executions. Finally, we focus on the shape of the executions and extract formal specifications to characterize their geometric patterns, which are particularly useful for analyzing time-series data with repeated patterns, such as cardiac activity or voltage signals. We evaluate the performance of each proposed method on several case studies, as well as the interpretability of the learned formulas.