Specifying Monitors for Autonomous Cyber-Physical Systems

Abstract

In this thesis, we investigate and apply specification-based monitoring for autonomous cyber-physical systems, such as unmanned aerial vehicles (UAV). The aim is to support development and ensure safe and correct operation. First, we show how aviation safety documents map to monitoring and how system behaviors are formalized. In particular, we propose temporal behavior trees (TBT), which build upon the widely used Behavior Tree (BT) framework for robotic task execution by combining it with temporal languages. TBTs provide a modular structure for decomposing complex tasks and enable retrofitting monitoring into applications that use BT. Second, we present offline monitoring algorithms that analyze system log files post-execution. We introduce trace segmentation that splits the trace into seg-ments and assigns them portions of the specification. This helps to understand which parts of the specification are violated and require further development. We then propose trace repair that minimally modifies a trace that violates its specification so that it satisfies it. Our experiments include an autonomous landing of a UAV on a ship and demonstrate their practical use. Last, we present tools for online monitoring that ease the integration of specified monitors and validate these monitors in real-world flight tests. The results confirm the effectiveness of our specified monitors in safeguarding both machine learning components and UAV operations.

In dieser Arbeit untersuchen und wenden wir spezifikationsbasiertes Monitoring für autonome cyber-physische Systeme wie unbemannte Luftfahrzeuge (UAVs) an, um die Entwicklung zu unterstützen und einen sicheren Betrieb zu gewährleisten. In Teil I zeigen wir, wie Luftfahrtdokumenten auf Monitoring abgebildet werden und wie Systemverhalten formalisiert werden. Wir führen Temporale Behavior Trees (TBT) ein, die auf dem verbreiteten Behavior-Tree-Framework (BT) für robotische Aufgabensteuerung aufbauen und es um temporale Sprachen erweitern. TBTs bieten eine modulare Struktur zur Zerlegung komplexer Aufgaben und ermöglichen die nachträgliche Integration von Monitoring in BT-Anwendungen. In Teil II stellen wir Offline-Monitoring-Algorithmen vor, die Logdateien analysieren. Zunächst führen wir Trace-Segmentierung ein, die die Ausführung in Segmente teilt und diesen Teile der Spezifikation zuweist. Dies hilft zu verstehen welche Teile weiteren Entwicklungsbedarf haben. Anschließend stellen wir Trace-Reparatur vor, die eine verletzende Ausführung minimal modifiziert, sodass sie die Spezifikation erfüllt. Experimente, darunter die autonome Landung eines UAV auf einem Schiff, zeigen die praktische Anwendbarkeit. In Teil III zeigen wir Werkzeuge für das Online-Monitoring, die die Integration spezifizierter Monitore vereinfachen und validieren diese in Flugtests. Die Ergebnisse bestätigen die Wirksamkeit beim Schutz vor maschineller Lernkomponenten und des UAV Betriebs.