Verifiable Runtime Monitor Generation for Lola Specifications

Stefan Oswald

Runtime monitoring nowadays is commonly used to verify program behavior whenever static verification fails. This can happen either due to missing information about input data or because of insufficient analysis precision. A monitor supervises a program with respect to a specification and reports program behavior violating the specification. So far, there are no formal guarantees that the monitor reflects the semantics of the underlying specification correctly. It is important to verify the monitor’s behavior to ensure the soundness and completeness of all specification violation reports. In this thesis, we introduce a translation algorithm to transform a Lola specification into a Viper program. Lola is a specification language for formalizing the correct behavior of a synchronous system. The language Viper provides a static verification toolchain and is used to prove the functional correctness of programs. The generated program models the runtime monitor and is annotated with verification conditions. With this, we prove the correctness of the monitor and examine the behavior of a Lola monitor in a concurrent context. We determine all computations within the specification that can be processed in parallel and show the interleaving invariance and correctness of the monitors computations.

Bachelor Thesis.

(pdf)