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.
Introduction Model checking (MC) [
Despite its advantages, RV is limited when compared to verification techniques such as MC because
certain correctness properties cannot be verified at runtime [
Monitorable Fragments ϕ, φ ∈ μHML ::= tt | ϕ ∨ φ | hαiϕ | min X.ϕ | X (truth) (disjunction) (possibility) (min. fixpoint) (rec. variable)
Jtt, ρK Jϕ1∨ϕ2, ρK
Jhαiϕ, ρK JminX.ϕ, ρK
JX, ρK d=ef Sta ddeeff Jϕ1, ρK ∪ Jϕ2, ρK = = s | ∃r.s −α→ r and r ∈ Jϕ, ρK d=ef T {S ∈ Sta | Jϕ, ρ[X 7→ S]K ⊆ S} d=ef ρ(X) | ff | ϕ ∧ φ | [α]ϕ | max X.ϕ (falsehood) (conjunction) (necessity) (max. fixpoint)
Jff, ρK Jϕ1∧ϕ2, ρK
J[α]ϕ, ρK
JmaxX.ϕ, ρK
def
= ∅
ddeeff Jϕ1, ρK ∩ Jϕ2, ρK
=
= s | ∀r.s −α→ r implies r ∈ Jϕ, ρK
d=ef S {S ∈ Sta | S ⊆ Jϕ, ρ[X 7→ S]K}
θ, ϑ ∈ sHML ::= tt
π, $ ∈ cHML ::= tt
| ff
| ff
| [α]θ
| hαiπ
| θ∧ϑ
| π∨$
| max X.θ
| min X.π
| X
| X
Syntax
Semantics
Hennessy-Milner Logic with Recursion (μHML) RV’s limits in terms of verifiable properties is
evidenced more for branching-time logics, that are able to express properties describing behaviour over
multiple system executions. In recent work [
Extending the applicability of monitoring towards a combined verification We build on the
findings of [
(haihbitt) ∨ (hai[c]ff)
whereby we note that the subformula haihbitt is runtime verifiable, according to [
We therefore aim to devise general analysis techniques that reformulate any μHML formula into either conjunctions or disjunctions, i.e., ϕRV ∧ ϕMC or ϕRV ∨ ϕMC, where ϕRV and ϕMC denote the runtime-verifiable and model-checkable formula components, respectively. From a software engineering perspective, we envisage at least two ways how this decomposition between pre- and post-deployment verification can be fruitful: 1. The ensuing combined approach may be used as a means to minimise the verification effort required prior to the deployment of a system. E.g., in the case of (2), the model-checked subformula ϕMC = hai[c]ff is smaller than the full formula (1), since we would be offloading a degree of verification onto the runtime phase when runtime-verifying for ϕRV = haihbitt. Moreover, for disjunction decompositions such as (2), the satisfaction of ϕMC prior to deployment obviates the need for any runtime analysis, minimising runtime overheads (a dual argument applies for conjunction decompositions and ϕMC violations). 2. In settings where software correctness is desirable but not essential, a combined approach can be used as a means to circumvent full-blown MC. Specifically, instead of model-checking for (1), a system may be runtime-verified for ϕRV = haihbitt during its pilot launch, acting as a vetting phase: if ϕRV is satisfied during RV, this means that, by (2), (1) is satisfied as well; if not, we then proceed to model-check the system offline wrt. ϕMC = hai[c]ff.
A partial solution based on modal transition systems and modal refinement From a technical
point of view, the problem amounts, to computing the maximal monitorable semantic fragment of a given
μHML formula ϕ, that is, the formula ψ such that
• ψ ∈ cHML (ψ is positively monitorable),
• JψK ⊆ JϕK (every process that satisfies ψ also satisfies ϕ, i.e, ψ is a semantic fragment of ϕ),
• for every ψ0 ∈ cHML, we have that Jψ0K ⊆ J K ψ (ψ is maximal)
ϕ implies Jψ0K ⊆ J K
Dually, for the case of negatively monitorable formulas (fragment sHML), we are interested in the minimal
monitorable formula of which ϕ is a semantic fragment; we focus on the former formulation only since the
latter one can be solved by exploiting the duality between the two fragments (as in [
Instead of trying to obtain the desired formula through syntactic transformations, we adopt a semantic
approach that proved itself successful for the logic HML, i.e., the fragment of μHML devoid of fixpoint
operators. We first transform the input formula into a modal transition system (MTS ) [
Future directions Extending our approach to the full μHML remains an open issue: for this purpose,
MTSs should be extended with cycles so as to enable them to “mimic” fixpoint operators, which somehow
correspond to recursion. Once this obstacle is solved, we can also investigate the application of our
methods to the linear-time setting, where there are still formulas that are not monitorable [
Another direction we intend to pursue is that of extending our techniques to settings with enriched
monitoring capabilities. A number of these settings have recently been investigated for the logic μHML
in the work [