Specification Mining for Cyber-Physical Systems

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.