Runtime Monitoring with Lola
Sebastian Schirmer
Runtime monitoring is a formal method for analyzing system executions. This analysis improves the confidence in the behavior of the system, either by improving the comprehension of the system or by checking the adherence of desirable properties. Monitoring can be used offline based on log files but also online along with the system being executed. The latter facilitates feedback at runtime. A stream-based specification language for the desirable properties is Lola. Given a set of input streams, a set of output streams is evaluated. Lola is kept simple and expressive and, hence, closes the gap between temporal logic and hand-written monitor code.
The DLR ARTIS framework is used for research on autonomy concepts, applications, and implementations for unmanned aircrafts. Important aspects of increasing autonomy involve correctness, safety, robustness, and system health management. In all of these aspects, runtime monitoring is a useful method to support the task of their implementations.
In this thesis, the applicability of Lola in the context of unmanned aircraft is elaborated. Based on interviews with DLR engineers, desirable properties are formalized in Lola specifications. In addition, the main contribution of this thesis is to adapt Lola to the domain requirements. Therefore, the Lola specification language is extended by new operators to increase its usability and expressiveness. For offline monitoring, existing logged flight data is analyzed and the usage of Lola in practice is examined. For online monitoring, DLR’s available software-in-the-loop and hardware-in-the-loop simulations are used to evaluate the impact of monitoring on the system. In both monitoring cases, Lola is efficient and fast enough and, thus, can be used in practice. The specifications show that Lola is capable of expressing required properties. Further, in the online experiments, the effect of Lola on the system is hardly measurable.
Master Thesis.