=Paper=
{{Paper
|id=Vol-2308/aviose2019paper05
|storemode=property
|title=Using Runtime Monitoring to Enhance Offline Analysis
|pdfUrl=https://ceur-ws.org/Vol-2308/aviose2019paper05.pdf
|volume=Vol-2308
|authors=Sebastian Schirmer,Sebastian Benders
|dblpUrl=https://dblp.org/rec/conf/se/SchirmerB19
}}
==Using Runtime Monitoring to Enhance Offline Analysis==
https://ceur-ws.org/Vol-2308/aviose2019paper05.pdf
Using Runtime Monitoring
to Enhance Offline Analysis
Sebastian Schirmer Sebastian Benders
Institute of Flight Systems, dept. Unmanned Aircraft Institute of Flight Systems, dept. Unmanned Aircraft
German Aerospace Center (DLR) German Aerospace Center (DLR)
Braunschweig, Germany Braunschweig, Germany
sebastian.schirmer@dlr.de sebastian.benders@dlr.de
Abstract—Offline log file analysis of unmanned aircraft systems ators [1], and sensors were installed [2]. During operation of
is a challenging experts task. Due to more automation, the the unmanned aircraft the subsystem which is responsible for
amount and complexity of logged data increases. Experts need controlling the core avionics of the aircraft, e.g. the actuators
support, for instance by automatically generating additional sta-
tistical information or by correlating data. Runtime Monitoring is and the engine control, generates more than 370 logged system
a formal method for analyzing system executions. It allows users states and sensor signals in 16 log files [2]. Additionally, flight
to express temporal properties in a formal language which then state sensors as well as the automatic flight control system are
can be used for the generation of a corresponding monitor. In generating log files. A pure manual inspection of the log files
this paper, we propose to integrate Runtime Monitoring into our is inefficient. The proposed approach automates simple checks
offline analysis process. We show how the results of the monitor
can be used to enhance the log file analysis and, therefore, support and supports the analysis by adding statistical information to
the expert. Specifically, we use the stream-based specification the visualization pointing towards potential errors identified by
language L OLA and apply it to the log files of an unmanned the monitors. Therefore, the approach reduces the workload of
cargo aircraft. the operating crew and delivers quick evaluation results right
Index Terms—Aerospace, Runtime Monitoring, L OLA, Offline in the field during flight-testing.
Analysis, Log File Analysis, Unmanned Aircraft Systems
II. R ELATED W ORK
I. I NTRODUCTION
Work in the field of RM mostly focuses on the online use-
Safety is one of the biggest concerns in aviation. During case, i.e. while operating the system. Among others, RM has
development and operation, the state of the aircraft needs to been used for unmanned aircraft systems [3], smart homes [4],
be captured and degradation of the system has to be detected cars [5], and ground rovers [6]. In [7], RM was used in an
to take suitable counter-measures, e.g. to replace damaged or offline fashion to support testing of spacecraft flight software
worn parts. Therefore, relevant data is stored and analyzed for the NASA 2011 Mars mission MSL (Mars Science Labra-
subsequently. Offline analysis is a challenging task and even tory). Instead of a stream-based specification language, the
more complicated due to the higher degree of automation rule-based specification language of the tool LOGSCOPE
induced by unmanned aircraft. The amount and complexity of was applied. Here, we focus more on the integration of RM
relevant data has increased. One established way for analysis into the current offline analysis workflow for a single log file,
is to generate plots from the log files for visual inspection i.e. how to enhance the analysis by RM. In [8], the problem
by an expert. There, the correlation of data is a challenging, of synchronizing different log files is considered. There, the
tedious, and repeating task. In short, it is error-prone. system is distributed and concurrent and, therefore, the locally
In this paper, we propose to integrate Runtime Monitoring observed, time stamped, and logged data might not be in order.
(RM) into our offline analysis process. We further show how One established way for data analysis is to use libraries like
to use the monitor results to enhance the offline analysis sup- the python data analysis library PANDAS [9]. It is open-source,
porting the expert. RM allows to express temporal properties easy-to-use, and expressive. Data queries can be easily stated,
in a formal and descriptive way which can be automatically e.g. data[data.a>data.b] returns the data where a>b.
translated into a corresponding correct monitor. Another ben- However, since it is based on python, it is more imperative
efit is the separation of the analysis code and the specified and it does not natively allow temporal queries, whose imple-
log file properties which improves the understanding and the mentations are prone to errors.
maintenance. The work is motivated by the in-house DLR
(German Aerospace Center) project ALAADy (Automated III. A PPROACH
Low-Altitude Air Delivery). This prototype aircraft is based In order to support the offline log file analysis, we propose
on a manned ultralight gyrocopter which was converted to to integrate RM into the analysis workflow. RM is a formal
an unmanned cargo aircraft with a payload of 200 kg. For method for analyzing system executions. The correct behavior
this purpose avionics such as flight control computers, actu- and statistical measurements of the systems are declared in
AvioSE 2019: 1st Workshop on Avionics Systems and Software Engineering @ SE19, Stuttgart, Germany 83
a specification file. Based on the specification, a monitor is const := //constants
generated which checks whether the specification is fulfilled ...
during system execution. Due to this profiling of the system, input //input streams
...
the confidence in the system is improved. The events and
output := //output streams
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 Listing 1: Basic L OLA specification structure
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 A L OLA specification consists of a set of independent input
are depicted in Figure 1. As specification language, we chose streams and a set of dependent output streams. The basic
L OLA which is presented in Section III-A structure of a L OLA specification is depicted in Listing 1.
Output streams can be used to represent an error, diagno-
Currently, log files are inspected manually to find unex-
sis reports, or quantitative statistics. Input streams represent
pected system behavior. The major analysis is done by review-
signals of the system under scrutiny. All streams are evalu-
ing generated signal graphs. Based on these plots, an expert
ated at the pace of a synchronous clock. For asynchronous
has to decide whether the system did operate nominally or
systems, synchronization techniques like sample and hold
not. The approach, described in Section III-B, allows experts to
can be applied. Note that since L OLA basically describes a
explicitly state assumptions on the system behavior in a formal
system of equations, the order of input and output declarations
and unambiguous way and to automatically incorporate the
is irrelevant for the underlying evaluation algorithm which
analysis results into the normal workflow. We show examples
improves the usage and the maintainability. Values of output
of the enhanced offline analysis using RM in Section III-C.
streams are defined by their respective stream expression. A
stream expression can refer to previous, present, or possible
A. Formal Specification Language L OLA
future values of streams (both, input and output streams).
L OLA is a stream-based formal specification language for Further, the streams are typed (e.g binary, integer, double)
system online and offline monitoring. Originally, L OLA was and incrementally computable statistics can be specified. The
designed for synchronous systems including circuits and em- so called dependency graph [10] is used to capture the
bedded systems [10] and, lately, extended for network mon- dependencies between the streams, to identify whether a
itoring [11]. More recently, RTLOLA [12] was introduced, given specification is efficiently monitorable. Intuitively, this
which extends previous versions by sliding windows over real- syntactic analysis states that the specification does not contain
time intervals with aggregation functions. The corresponding unbounded future stream accesses, i.e. the time until the
L OLA tool [13] is actively developed at Saarland University. output stream is evaluated is bounded. This allows to make
Here, we remain within the more basic L OLA fragment statements about the memory consumption, e.g. only constant
described in [14]. In a previous work, L OLA was used in an memory is required. The key features of L OLA, which lead
online monitoring setting [15] which indicates its applicability. to its usage, compared to other temporal formal languages
There, an observation was that the development of specifi- (e.g. linear-time temporal logic), are: its descriptive nature,
cations for the online usage can be significantly supported its structurability, and the resemblance of expressions with
by testing them offline based on column-oriented log files. writing actual programs instead of abstract logical formulas.
As a side-effect, the understanding of the system was greatly Further, especially temporal properties expressed in L OLA are
improved which motivated this approach. easier to understand and to maintain compared to handwritten
code. Additionally, when operating several aircraft, such a
generic solution is highly desirable. Listing 2 shows a simple
Offline Online L OLA specification to compute the average velocity. The
example uses one input stream vel for the current velocity
Log File System of a vehicle and two output streams. The output vel_sum
is an auxiliary stream which incrementally computes the sum
Instrumentation over the seen velocities by accessing the previous value of
Events Feedback vel_sum and the current velocity. The offset operator s[x,y]
handles the access to previous (i.e. x < 0), present (i.e. x = 0),
Specification Monitor Verdict or future (i.e. x > 0) stream values of the stream s. The
Fig. 1: Based on a specification, a monitor is generated
which checks the adherence to a specified system behavior. input double vel
In offline monitoring, the system execution has finished and output double vel_sum := vel_sum[-1, 0.0] + vel
the log file is completely available. In online monitoring, the output double vel_avg := vel_sum / double(position+1)
execution is still ongoing and therefore the sequence of events
is continuously extended. Listing 2: Computation of the average velocity.
AvioSE 2019: 1st Workshop on Avionics Systems and Software Engineering @ SE19, Stuttgart, Germany 84
ace_basic -> actuator_left, actuator_nose_wheel,
actuator_right, actuator_rudder
ace_left_specific -> actuator_left
Listing 3: Specification-to-logfile mapping. The L OLA specifi-
cation 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.
B. Enhancing Offline Analysis
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 L OLA specification. Fig. 2: Illustration of the proposed offline analysis approach
Based on these specifications monitors will be generated which using RM. Meta-information is inferred to enhance log files.
analyze the files. Specifications can be named and mapped to The extended log file is visualized and the meta-information
specific log files. An example mapping is shown in Listing 3. is used to point out erroneous regions to the user.
This is especially interesting for recurring specifications
which can be declared in separate specification files and
then automatically checked on the mapped log files by the
reused, e.g. timing properties. An example L OLA specification
generated monitors. After the analysis due to the monitors,
concerning timing is shown in Listing 4. Typically, time
the verdicts, e.g. the mentioned maximal values or raised
is captured via timestamps in log files. Interesting timing
notification, can be used to enhance the used visualization.
properties are the average, minimal, and maximal time jumps
Colors indicate whether the values for the respective plots
(t_jmp). Maximal and minimal values indicate frozen and
were involved in a notified violation, i.e. a violation of an
rapid system states, respectively. Also, time jumps larger than
explicitly stated assumption. In Figure 2, the first two plots
the given threshold t_safe can be detected and reported.
are healthy but some notifications where raised for plot p. In
Note that a L OLA specification can be easily extended by
both cases, the users preferred visualization tool-chain can be
an user due to the irrelevance of the stream declaration
enhanced by statistical information. For the erroneous case,
ordering. For instance, by adding an additional output stream,
the monitor result can guide the expert’s attention towards
the number of violations can be counted. The properties are
interesting regions.
Considering the visualization of plot p shown in Figure 2,
input double time_s, time_us assuming the actuator position over time is depicted and timing
output double time := time_s + time_us / 1000000.0 notifications (see Listing 4) were evaluated, an expert can
output double t_jmp := time - time[-1,0.0] see that each time a time jump occurred, the position of the
//User notification if t_jmp > t_safe actuator changed.
const double t_safe := 0.05
trigger t_jmp > t_safe with "VIOLATION: time jump!"
//Statistical information C. Example Properties
output double t_sum := t_sum[-1, 0.0] + t_jmp Actually, the presented identification of time jumps, i.e. tem-
output 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
Listing 4: Given the current timestamp (time_s,time_us), to using scatter plots. Also, humans tend to extend their
the elapsed time t_jmp is computed. Based on the com- tolerance limit over time, e.g. due to optimism, self-serving
parison with the constant t_safe a trigger notification is bias, or anchoring [16]. Hard thresholds explicitly stated in a
raised representing a too large time jump. Further, t_sum specification do not only allow to reduce the reliance on gut-
aggregates t_jmp which can be used to compute the average feeling but also allow to identify anomalies across different
time jumps t_avg. The output streams t_max and t_min log files. Using this approach, we cannot only automatically
compute the maximal and the minimal time jump, respectively. check whether jumps exist in the current log files, we can also
AvioSE 2019: 1st Workshop on Avionics Systems and Software Engineering @ SE19, Stuttgart, Germany 85
make new assumptions, e.g. decrease t_safe, and re-evaluate IV. C ONCLUSION
the specification on the current and the historical log files. In We have presented RM and the specification language
the following, we show other simple but helpful properties of L OLA. Further, we motivated why and showed how RM can
ace_basic and ace_left_specific (see Listing 3): be used for offline log file analysis. Specifically, we illustrated
• Each actuator implements a state machine. State changes how manual inspection due to visualization can be enhanced
are logged as device status. In the end, the sequence of due to the outputs of the formally specified monitors. We plan
device states represent a valid execution. to fully implement the integration of runtime monitors into our
• Bounds on the demanded actuator position differ for each offline analysis tool-chain. Also, the reasoning across different
actuator and should never be exceeded to avoid defects. log files is very helpful and will be central since future
• The mechanical loads of the actuators and therefore their systems tend to be highly distributed. Currently, L OLA is able
consumption of current differ. to read column-oriented .csv and .dat files. Accepting other
• Statistical information on the average, maximal, and min- data formats, e.g. CDF, NetCDF, HDF, would improve the
imal values for current consumption, timing, velocity, and general applicability. In future, we will investigate how offline
voltage are useful to get more insights into the system. monitoring enhances online monitoring of future sessions and,
• The relation between consumption of current and position vice versa, how online monitoring helps to provide targets to
demands can be analyzed to differentiate between internal detailed offline monitoring of the same session. Further, the
and external errors. benefits of the proposed approach in regards of cost savings,
• Estimation of the time difference between the position usability, and quality improvements compared to a manual
demand and the time when the target position was inspection will be investigated.
reached.
R EFERENCES
Note that these are just examples for a single actuator log
[1] A. Bierig, S. Lorenz, M. Rahm, P. Gallun, “Design considerations and
file. Figure 3 shows a visualization example utilizing the test of the flight control actuators for a demonstrator for an unmanned
monitoring results. The orange and the green line indicate freight transportation aircraft”, Recent Advances in Aerospace Actuation
the specified upper and lower bound on the consumption Systems and Components, 2018
[2] S. Benders, L. Goormann, S. Lorenz, J.C. Dauer, “Softwarearchitek-
of current, respectively. The red regions show where trigger tur für einen unbemannten Luftfrachttransportdemonstrator”, Deutscher
notifications were raised by a monitor. Here, red regions Luft- und Raumfahrtkongress, 2018
indicate an increased current consumption despite no actuator [3] T. Reinbacher, K.Y. Rozier, J. Schumann, “Temporal-Logic Based
Runtime Observer Pairs for System Health Management of Real-Time
position demand was commanded previously. In fact, consid- Systems”, Tools and Algorithms for the Construction and Analysis of
ering the first red region, the increased current consumption Systems (TACAS), 2014
is related to the initialization procedure of the actuator. With [4] A. El-Hokayem, Y. Falcone, “Bringing Runtime Verification Home”,
Runtime Verification - 18th International Conference (RV), 2018
the specification violations in mind, i.e. the second red region [5] J.V. Deshmukh, A. Donzé, S. Gosh, X. Jin, G. Juniwal, S.A. Seshia,
around 400 s and the upper bound violation around 850 s, the “Robust Online Monitoring of Signal Temporal Logic”, Runtime Veri-
expert can now examine the log files in detail to determine fication - 15th International Conference (RV), 2015
[6] D. Phan, J. Yang, M. Clark, R. Grosu, J. Schierman, S. Smolka, S.
the root cause. Stoller, “A Component-Based Simplex Architecture for High-Assurance
Cyber-Physical Systems”, 17th International conference on application
15 of concurrency to system design (ACSD), 2017
[7] H. Barringer, K. Havelund, D. Rydeheard, A. Groce, “Rule Systems for
Runtime Verification: A Short Tutorial”, Runtime Verification Lecture
10 Notes in Computer Science, 2009
[8] D. Basin, M. Harvan, F. Klaedtke, E. Zalinescu, “Monitoring Data Usage
5 in Distributed Systems”, IEEE Transactions on Software Engineering,
2013
[9] Python Data Analysis Library - pandas, https://pandas.pydata.org/, last
current [A]
0 visited: 05.01.2019
[10] B. D’Angelo, S. Sankaranarayanan, C. Sánchez, W. Robinson, B.
Finkbeiner, H. B. Sipma, S. Mehrotra, Z. Manna, “Lola: Runtime
5 Monitoring of Synchronous Systems”, 12th International Symposium
on Temporal Representation and Reasoning (TIME’05), 2005
[11] P. Faymonville, B. Finkbeiner, S. Schirmer, H. Torfah, “A Stream-Based
10 Specification Language for Network Monitoring”, Runtime Verification
- 16th International Conference (RV), 2016
15
Monitor notification Current upper bound [12] P. Faymonville, B. Finkbeiner, M. Schwenger, H. Tor-
Current Current lower bound fah, “Real-time Stream-based Monitoring”, Available on
https://arxiv.org/abs/1711.03829
0 200 400 600 800 1000 [13] Lola - Stream-based Runtime Monitoring, https://www.react.uni-
time [s] saarland.de/tools/lola/, last visited: 07.01.2019
Fig. 3: Current consumption of an actuator with specified [14] S. Schirmer, “Runtime Monitoring with Lola”, Master’s Thesis, 2016
[15] F-M. Adolf, P. Faymonville, B. Finkbeiner, S. Schirmer, C. Torens,
lower and upper bounds. Red regions indicate a notification “Stream Runtime Monitoring on UAS”, Runtime Verification - 17th
due to a comparison between current consumption and actu- International Conference (RV), 2017
ator position demand. [16] R. Collins, B. Leathley, “The Psychology of Errors in the Engineering
Process”, Safety and Reliability, 1995
AvioSE 2019: 1st Workshop on Avionics Systems and Software Engineering @ SE19, Stuttgart, Germany 86