Pushing runtime verification to the limit : may process semantics be with us

We propose a combined approach that permits automated formal verification to be spread across the pre- and post-deployment phases of a system development, with the aim of calibrating the management of the verification burden. Our approach combines standard model checking methods with runtime verification, a relatively novel formal technique that verifies a system during its execution. We carry out our study in terms of the Hennessy-Milner Logic, a branching-time logic for specifying reactive system correctness. Whereas we will be mainly concerned with limiting the model checking verification burden, runtime verification has been shown to handle a strict subset of the expressible properties in our logic of study, posing constraints on what can be shifted to the post-deployment phase. We present a solution, based on modal transition systems and modal refinement, for the fragment of the Hennessy-Milner Logic devoid of recursion, i.e., without least and greatest fixpoint operators.This work is partially supported by the Italian INdAM-GNCS project Metodi formali per tecniche di verifica combinata, the Icelandic Research Fund project TheoFoMon: Theoretical Foundations for Monitorability (No.163406-051), and the project BehAPI, funded by the EU H2020 RISE programme under the Marie Skłodowska-Curie grant agreement (No.778233).peer-reviewe