Tracing Correctness: A Practical Approach to Traceable Runtime Monitoring
Jan Baumeister
The established approach to check the correctness of a cyber-physical system is to verify all possible executions statically. With their increasing autonomy, verifying all traces develops into a harder problem. To handle the increased complexity, runtime monitoring verifies the system dynamically.
RTLola is a stream-based specification language to express complex real-time constraints that provides different static analyses as the determination of an upper bound on the required memory. The underlying monitoring framework, StreamLAB, uses these analyses and interprets the given RTLola specification. However, to find an industrial application for aerial vehicles, a certification by the Federal Aviation Administration (FAA) or the European Union Aviation Safety Agency (EASA) is needed. Part of this certification process is to show that the product is traceable, i.e., describing the relationship between the specification language and the software. One advantage of a traceable implementation is the identification and documentation of each code fragment and reason for their existence. For an interpreted monitor, like the StreamLAB framework, it is unfeasible to show this property.
Recent work introduces a hardware-based approach, compiling VHDL code out of an RTLola specification. This VHDL code can then be synthesized into an FPGA implementation. This thesis presents a prototype implementation of this compilation concerning a traceable result. It additionally describes the integration of a synthesized monitor into the unmanned aerial vehicle superARTIS by the German Aerospace Center (DLR).
Master Thesis.