-Offline log file analysis of unmanned aircraft systems is a challenging experts task. Due to more automation, the amount and complexity of logged data increases. Experts need support, for instance by automatically generating additional statistical information or by correlating data. Runtime Monitoring is a formal method for analyzing system executions. It allows users to express temporal properties in a formal language which then can be used for the generation of a corresponding monitor. In this paper, we propose to integrate Runtime Monitoring into our offline analysis process. We show how the results of the monitor can be used to enhance the log file analysis and, therefore, support the expert. Specifically, we use the stream-based specification language LOLA and apply it to the log files of an unmanned cargo aircraft. Index Terms-Aerospace, Runtime Monitoring, LOLA, Offline Analysis, Log File Analysis, Unmanned Aircraft Systems II. RELATED WORK
Safety is one of the biggest concerns in aviation. During development and operation, the state of the aircraft needs to be captured and degradation of the system has to be detected to take suitable counter-measures, e.g. to replace damaged or worn parts. Therefore, relevant data is stored and analyzed subsequently. Offline analysis is a challenging task and even more complicated due to the higher degree of automation induced by unmanned aircraft. The amount and complexity of relevant data has increased. One established way for analysis is to generate plots from the log files for visual inspection by an expert. There, the correlation of data is a challenging, tedious, and repeating task. In short, it is error-prone.
In this paper, we propose to integrate Runtime Monitoring
(RM) into our offline analysis process. We further show how
to use the monitor results to enhance the offline analysis
supporting the expert. RM allows to express temporal properties
in a formal and descriptive way which can be automatically
translated into a corresponding correct monitor. Another
benefit is the separation of the analysis code and the specified
log file properties which improves the understanding and the
maintenance. The work is motivated by the in-house DLR
(German Aerospace Center) project ALAADy (Automated
Low-Altitude Air Delivery). This prototype aircraft is based
on a manned ultralight gyrocopter which was converted to
an unmanned cargo aircraft with a payload of 200 kg. For
this purpose avionics such as flight control computers,
actuators [
Work in the field of RM mostly focuses on the online
usecase, i.e. while operating the system. Among others, RM has
been used for unmanned aircraft systems [
One established way for data analysis is to use libraries like
the python data analysis library PANDAS [
In order to support the offline log file analysis, we propose to integrate RM into the analysis workflow. RM is a formal method for analyzing system executions. The correct behavior and statistical measurements of the systems are declared in a specification file. Based on the specification, a monitor is generated which checks whether the specification is fulfilled during system execution. Due to this profiling of the system, the confidence in the system is improved. The events and signal data are either received due to system instrumentation during operation or read from log files afterwards. The former is referred to as online monitoring and the latter is referred to as offline monitoring. In both cases, the monitor outputs a verdict as a result which represents the adherence of the execution to the specification. Online and offline monitoring are depicted in Figure 1. As specification language, we chose LOLA which is presented in Section III-A
Currently, log files are inspected manually to find unexpected system behavior. The major analysis is done by reviewing generated signal graphs. Based on these plots, an expert has to decide whether the system did operate nominally or not. The approach, described in Section III-B, allows experts to explicitly state assumptions on the system behavior in a formal and unambiguous way and to automatically incorporate the analysis results into the normal workflow. We show examples of the enhanced offline analysis using RM in Section III-C.
LOLA is a stream-based formal specification language for
system online and offline monitoring. Originally, LOLA was
designed for synchronous systems including circuits and
embedded systems [
Offline
Online
Feedback
Fig. 1: Based on a specification, a monitor is generated which checks the adherence to a specified system behavior. In offline monitoring, the system execution has finished and the log file is completely available. In online monitoring, the execution is still ongoing and therefore the sequence of events is continuously extended. const <type> <name> := <value> //constants ... input <type> <name> //input streams ... output <type> <name> := <expression> //output streams ...
A LOLA specification consists of a set of independent input
streams and a set of dependent output streams. The basic
structure of a LOLA specification is depicted in Listing 1.
Output streams can be used to represent an error,
diagnosis reports, or quantitative statistics. Input streams represent
signals of the system under scrutiny. All streams are
evaluated at the pace of a synchronous clock. For asynchronous
systems, synchronization techniques like sample and hold
can be applied. Note that since LOLA basically describes a
system of equations, the order of input and output declarations
is irrelevant for the underlying evaluation algorithm which
improves the usage and the maintainability. Values of output
streams are defined by their respective stream expression. A
stream expression can refer to previous, present, or possible
future values of streams (both, input and output streams).
Further, the streams are typed (e.g binary, integer, double)
and incrementally computable statistics can be specified. The
so called dependency graph [
ace_basic -> actuator_left, actuator_nose_wheel, actuator_right, actuator_rudder ace_left_specific -> actuator_left Listing 3: Specification-to-logfile mapping. The LOLA specification ace_basic is applied to all four actuators whereas ace_left_specific is only used for the left actuator. default value y is used for accesses past the end or before the beginning of a stream. In Listing 2, -1 indicates the access to the previous value and 0.0 is used as a default value at the first position. Finally, using the keyword position, representing the current step of the evaluation (starting from zero), the average velocity is computed in vel_avg.
The presented approach supports the analysis of log files, see Figure 2. During system tests, log files are generated which need to be reviewed. To support the manual inspection of each log file, we want to capture common erroneous and desired behaviors within a formal LOLA specification. Based on these specifications monitors will be generated which analyze the files. Specifications can be named and mapped to specific log files. An example mapping is shown in Listing 3.
This is especially interesting for recurring specifications which can be declared in separate specification files and reused, e.g. timing properties. An example LOLA specification concerning timing is shown in Listing 4. Typically, time is captured via timestamps in log files. Interesting timing properties are the average, minimal, and maximal time jumps (t_jmp). Maximal and minimal values indicate frozen and rapid system states, respectively. Also, time jumps larger than the given threshold t_safe can be detected and reported. Note that a LOLA specification can be easily extended by an user due to the irrelevance of the stream declaration ordering. For instance, by adding an additional output stream, the number of violations can be counted. The properties are Fig. 2: Illustration of the proposed offline analysis approach using RM. Meta-information is inferred to enhance log files.
then automatically checked on the mapped log files by the generated monitors. After the analysis due to the monitors, the verdicts, e.g. the mentioned maximal values or raised notification, can be used to enhance the used visualization.
Colors indicate whether the values for the respective plots were involved in a notified violation, i.e. a violation of an explicitly stated assumption. In Figure 2, the first two plots are healthy but some notifications where raised for plot p. In both cases, the users preferred visualization tool-chain can be enhanced by statistical information. For the erroneous case, the monitor result can guide the expert’s attention towards interesting regions.
Considering the visualization of plot p shown in Figure 2, assuming the actuator position over time is depicted and timing notifications (see Listing 4) were evaluated, an expert can see that each time a time jump occurred, the position of the actuator changed.
Listing 4: Given the current timestamp (time_s,time_us),
the elapsed time t_jmp is computed. Based on the
comparison with the constant t_safe a trigger notification is
raised representing a too large time jump. Further, t_sum
aggregates t_jmp which can be used to compute the average
time jumps t_avg. The output streams t_max and t_min
compute the maximal and the minimal time jump, respectively.
input double time_s, time_us
output double time := time_s + time_us / 1000000.0
output double t_jmp := time - time[-1,0.0]
//User notification if t_jmp > t_safe
const double t_safe := 0.05
/t/rSitgagetristti_cjamlp i>nfto_rsmaafteiownith "VIOLATION: time jump!" C. Example Properties
output double t_sum := t_sum[-1, 0.0] + t_jmp Actually, the presented identification of time jumps, i.e.
temoutput double t_avg := t_sum / (double(position+1))
output double t_max := max(t_jmp,t_max[-1,double_min]) poral system loss, was motivated by a real problem. Experts
output double t_min := min(t_jmp,t_min[-1,double_max]) rely on different types of visualization to identify errors.
Detecting time jumps using line plots is error-prone compared
to using scatter plots. Also, humans tend to extend their
tolerance limit over time, e.g. due to optimism, self-serving
bias, or anchoring [
Each actuator implements a state machine. State changes are logged as device status. In the end, the sequence of device states represent a valid execution.
Bounds on the demanded actuator position differ for each actuator and should never be exceeded to avoid defects.
The mechanical loads of the actuators and therefore their consumption of current differ.
Statistical information on the average, maximal, and minimal values for current consumption, timing, velocity, and voltage are useful to get more insights into the system.
demands can be analyzed to differentiate between internal and external errors.
Estimation of the time difference between the position demand and the time when the target position was reached.
Note that these are just examples for a single actuator log file. Figure 3 shows a visualization example utilizing the monitoring results. The orange and the green line indicate the specified upper and lower bound on the consumption of current, respectively. The red regions show where trigger notifications were raised by a monitor. Here, red regions indicate an increased current consumption despite no actuator position demand was commanded previously. In fact, considering the first red region, the increased current consumption is related to the initialization procedure of the actuator. With the specification violations in mind, i.e. the second red region around 400 s and the upper bound violation around 850 s, the expert can now examine the log files in detail to determine the root cause.
15 10 5 10 15
Monitor notification 0
Current 200 400
600 time [s]
Current upper bound Current lower bound 800 1000
We have presented RM and the specification language LOLA. Further, we motivated why and showed how RM can be used for offline log file analysis. Specifically, we illustrated how manual inspection due to visualization can be enhanced due to the outputs of the formally specified monitors. We plan to fully implement the integration of runtime monitors into our offline analysis tool-chain. Also, the reasoning across different log files is very helpful and will be central since future systems tend to be highly distributed. Currently, LOLA is able to read column-oriented .csv and .dat files. Accepting other data formats, e.g. CDF, NetCDF, HDF, would improve the general applicability. In future, we will investigate how offline monitoring enhances online monitoring of future sessions and, vice versa, how online monitoring helps to provide targets to detailed offline monitoring of the same session. Further, the benefits of the proposed approach in regards of cost savings, usability, and quality improvements compared to a manual inspection will be investigated.