Efficient Code Generation for Stream-based Specifications

Abstract - Zusammenfassung

In the field of Runtime Verification it is a common approach to use stream processing
languages to check certain properties on streams, generated by the observed program.
For example streams of current variable values can be monitored this way. In order
to satisfy the speed requirements in this field, it is advantageous to have the ability to
compile such languages to efficient machine code. In this thesis a compiler from TeSSLa
(Temporal Stream-based Specification Language) to Java and Rust source code will be
presented and its correctness will be proven. As datastructures, TeSSLa also supports
object datatypes. Concerning them, a method will be shown, how efficient memory
management in the generated code, and thus an advantage in runtime can be achieved.
This is done by using mutable datastructures instead of immutable ones, where possible.
In the last section the efficiency of the implementation of this compiler is measured and
compared to a TeSSLa interpreter.