Compiling Lola 2.0 to C

Christoph Rosenhauer

Runtime monitoring is a lightweight verification approach based on the extraction of information from a running system. This information is used to detect violations of a given specification to ensure the correctness of the system at runtime. Lola 2.0 is a simple and expressive specification language and stream processing engine for monitoring temporal properties and computing complex statistical measurements. It supports dynamic stream generation as well as parameterization with data. This enables monitoring of new subtasks on their own timescale. Lola 2.0 is currently applied to unmanned aircraft systems at DLR. For this purpose, specifications have so far only been evaluated by an interpreter. This thesis will change that, since a compiled C code monitor strongly improves the maintainability of a specification. Compared to the general interpreter code, the generated C code greatly eases the process of understanding and verifying the monitor. This enables the opportunity of easily modifying the C code monitor itself, whereby a higher flexibility in testing and also under actual deployment is granted. Furthermore, the compilation could speed up the monitoring process in general by eliminating the computational overhead that an interpreter brings along. In this thesis we present an approach to translate Lola 2.0 to C as well as the implementation of a compiler.

Bachelor Thesis.