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 segments 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.