Synthesising correct concurrent runtime monitors

Abstract

This paper studies the correctness of automated synthesis for concurrent monitors. We adapt a subset of the Hennessy-Milner logic with recursion (a reformulation of the modal μ-calculus) to specify safety properties for Erlang programs. We also define an automated translation from formulas in this sub-logic to concurrent Erlang monitors that detect formula violations at runtime. Subsequently, we formalise a novel definition for monitor correctness that incorporates monitor behaviour when instrumented with the program being monitored. Finally, we devise a sound technique that allows us to prove monitor correctness in stages; this technique is used to prove the correctness of our automated monitor synthesis.