Runtime verification tools must correctly establish a specification's validity or detect violations. This task is difficult, especially if the specification is given in an expressive declarative language, which demands a non-trivial monitoring algorithm. We use a proof assistant to not only solve this task, but also to gain confidence in our solution. We formally verify the correctness of a monitor for specifications given as formulas in metric first-order temporal logic in the Isabelle/HOL proof assistant. From our formalization, we extract an executable algorithm with correctness guarantees and use differential testing to find discrepancies in the outputs of two unverified monitors for first-order specification languages.
The final publication is available at link.springer.com.
Paper draft