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

Abstract

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.