We present methods for repairing traces against specifications given as temporal behavior trees (TBT). TBT are a specification formalism for action sequences in robotics and cyber-physical systems, where specifications of sub-behaviors, given in signal temporal logic, are composed using operators for sequential and parallel composition, fallbacks, and repetition. Trace repairs are useful to explain failures and as training examples that avoid the observed problems. In principle, repairs can be obtained via mixed-integer linear programming (MILP), but this is far too expensive for practical applications. We present two practical repair strategies: (1) incremental repair, which reduces the MILP by splitting the trace into segments, and (2) landmark-based repair, which solves the repair problem iteratively using TBT’s robust semantics as a heuristic that approximates MILP with more efficient linear programming. In our experiments, we were able to repair traces with more than 25 000 entries in under ten minutes, while MILP runs out of memory.

Abstract This paper reports on the integration of runtime monitoring into fully-electric aircraft designed by Volocopter, a German aircraft manufacturer of electric multi-rotor helicopters. The runtime monitor recognizes hazardous situations and system faults. Since the correct operation of the monitor is critical for the safety of the aircraft, the development of the monitor must follow strict aeronautical standards. This includes the integration of the monitor into different development environments, such as log-file analysis, hardware/software-in-the-loop testing, and test flights. We have used the stream-based monitoring framework RTLola to generate monitors for a range of requirements. In this paper, we present representative monitoring specifications and our lessons learned from integrating the generated monitors. Our main finding is that the specification and the integration need to be decoupled, because the specification remains stable throughout the development process, whereas the different development stages require a separate integration of the monitor into each environment. We achieve this decoupling with a novel abstraction layer in the monitoring framework that adapts the monitor to each environment without affecting the core component generated from the specification. The decoupling of the integration has also allowed us to react quickly to the frequent changes in the hardware and software environment of the monitor due to the fast-paced development of the aircraft in a startup company.

This paper presents temporal behavior trees (TBT), a specification formalism inspired by behavior trees that are commonly used to program robotic applications. We then introduce the concept of trace segmentation, wherein given a TBT specification and a trace, we split the trace optimally into sub-traces that are associated with various portions of the TBT specification. Segmentation of a trace then serves to explain precisely how a trace satisfies or violates a specification, and which portions of a specification are actually violated. We introduce the syntax and semantics of TBT and compare their expressiveness in relation to temporal logic. Next, we define robustness semantics for TBT specification with respect to a trace. Rather than a Boolean interpretation, the robustness provides a real-valued numerical outcome that quantifies how close or far away a trace is from satisfying or violating a TBT specification. We show that computing the robustness of a trace also segments it into subtraces.Finally, we provide efficient approximations for computing robustness and segmentation for long traces with guarantees on the result.We demonstrate how segmentations are useful through applications such as understanding how novice users pilot an aerial vehicle through a sequence of waypoints in desktop experiments and the offline monitoring of automated lander for a drone on a ship. Our case studies demonstrate how TBT specification and segmentation can be used to understand and interpret complex behaviors of humans and automation in cyber-physical systems.

We present our tool for the segmentation of temporal behavior trees (TBT), a novel formalism for monitoring specifications. TBTs can be easily retrofitted to behavior trees, commonly used to program robotic applications. Our tool supports the robustness semantics of TBT and generates trace segmentations. In other words, given a TBT specification and a trace, it determines the optimal assignment of TBT nodes to sub-traces. To illustrate its application, we use the example of an autonomous ship deck landing. We showcase the user inputs required and demonstrate how the outputs can be interpreted to identify challenging task aspects, contributing to a comprehensive system analysis.

Abstract Runtime monitoring is generally considered a light-weight alternative to formal verification. In safety-critical systems, however, the monitor itself is a critical component. For example, if the monitor is responsible for initiating emergency protocols, as proposed in a recent aviation standard, then the safety of the entire system critically depends on the correctness of the monitor. In this paper, we present a verification extension to theLolamonitoring language that extends the efficient specification of the monitor with Hoare-style annotations that guarantee the correctness of the monitor specification. We add two new operators, assume and assert, which specify assumptions of the monitor and expectations on its output, respectively. The validity of the annotations is established by an integratedSMTsolver. We report on experience in applying the approach to specifications from the avionics domain, where the annotation with assumptions and assertions has lead to the discovery of safety-critical errors in specifications. The errors range from incorrect default values in offset computations to complex algorithmic errors that result in unexpected temporal patterns. We also report how verified specifications can be monitored efficiently at runtime.

The autonomous control of unmanned aircraft is a highly safety-critical domain with great economic potential in a wide range of application areas, including logistics, agriculture, civil engineering, and disaster recovery. We report on the development of a dynamic monitoring framework for the DLR ARTIS (Autonomous Rotorcraft Testbed for Intelligent Systems) family of unmanned aircraft based on the formal specification language RTLola. RTLola is a stream-based specification language for real-time properties. An RTLola specification of hazardous situations and system failures is statically analyzed in terms of consistency and resource usage and then automatically translated into an FPGA-based monitor. Our approach leads to highly efficient, parallelized monitors with formal guarantees on the noninterference of the monitor with the normal operation of the autonomous system.