Synthesising Correct Concurrent Runtime Monitors - Runtime Verification - page 122

ensure that neither is violated. 8 A translation in terms of two concurrent (sub)monitors,
each analysing di

ff

erent parts of the trace so as to ensure the observation of its respec-
tive sub-formula, constitutes a natural synthesis of the conjunction formula in our tar-
get language: it adheres to recommended Erlang practices advocating for concurrency
wherever possible [7], but also allows us to benefit from the advantages of concurrent
monitors discussed in the Introduction.

Example 4 (Conjunction Formulas). Consider the two sHML formulas

α call ] max ( X α call ] X ) ϕ no dup ans [ , [ β ans ][ β ans ] ff ∧ [ β ans ][

ϕ react ans max ( Y , [ β ans ] ff ∧ [ α call ][ β ans ] Y )

Formula ϕ no dup ans requires that call actions α call are at most serviced by a single answer

action ϕ react ans requires that answer actions are only produced in

response to call actions. Although one can rephrase the conjunction of the two formulas
as a formula without a top-level conjunction, it is more straightforward to use two con-
current monitors executing in parallel (one for each sub-formula in

β ans , whereas formula

ϕ no dup ans ∧ϕ react ans ).
There are also other reasons why it would be beneficial to keep the sub-formulas sepa-
rate: for instance, keeping the formulas disentangled improves maintainability and sep-
aration of concerns when subformulas originate from distinct specifying parties.

Multiple conjunctions also arise indirectly when used under fix-point operators.
When synthesising concurrent monitors analysing separate branches of such recursive
properties, it is important to generate monitors that can dynamic spawn further sub-
monitors themselves as required at runtime, so as to keep the monitoring overheads to
a minimum.

Example 5 (Conjunctions and Fixpoints). Recall ϕ safe , from (2) in Ex. 2. Semantically,

the formula represents the infinite-depth tree with an infinite number of conjunctions,
depicted in Fig. 3(a). Although in practice, we cannot generate an infinite number of
concurrent monitors, ϕ safe will translate into possibly more than two concurrent moni-

tors executing in parallel.

Exp , takes a closed, guarded 9 sHML
formula and returns an Erlang function that is then parameterised by a map (encoded as
a list of tuples) from formula variables to other synthesised monitors of the same form.
The map encodes the variable bindings introduced by the construct max ( X

m

Our monitor synthesis, − :: sHML →

); it is used
for lazy recursive unrolling of formulas so as to minimize monitoring overhead. For in-
stance, when synthesising formula

,ϕ

ϕ safe from Ex. 2, the algorithm initially spawns only
two concurrent submonitors, one checking for the subformula [

α α β

][ ][ ] ff , and another

α

one checking for the formula [ ] X , as is depicted in Fig. 3(b). Whenever the rightmost

submonitor in Fig. 3(b) observes the action and reaches X , it unfolds X and spawns an

additonal submonitor as depicted in Fig. 3(c), thereby increasing the monitor overheads
incrementally.

α

8

Since conjunctions are found in many monitoring logics, the concepts discussed here extend
directly to other RV settings.

9

In guarded sHML formulas, variables appear only as a sub-formula of a necessity formula.