Information Technology Reference
In-Depth Information
Despite the technical discrepancies between the two definitions, e.g.,maximal versus
minimal fixpoints, a di
ff
erent model semantics etc., we show that Def. 2 corresponds,
in some sense, to the dual of Def. 1.
Theorem 1 (Correspondence).
∃
s
.
(
A
,
s
)
|=
v
ϕ
i
ff
A
|=
s
ϕ
Proof.
For the
if
case we prove the contrapositive, i.e.,that
∀
s
.
A
,
s
|=
v
ϕ
implies
A
|=
s
ϕ
by co-inductively showing that
R ={
(
A
,ϕ
)
|∀
s
.
A
,
s
|=
v
ϕ}
is a satisfaction relation. For
the
only-if
case we prove
∃
s
.
A
,
s
|=
v
ϕ
implies
A
|=
s
ϕ
by rule induction on
A
,
s
|=
v
ϕ
.
See [15] for details.
4
Correctness
Specifying online monitor correctness is complicated by the fact that, in general, we
have limited control over the behaviour of the systems being monitored. For starters, a
system that does not satisfy a property may still exhibit runtime behaviour that does not
violate it, as discussed earlier in the case of system
A
3
of Ex. 2 and Ex. 3. We deal with
system non-determinism by only requiring monitor detection when the system performs
a violating execution: this can be expressed through the violation relation of Def. 2.
At runtime, a system may also interfere with the execution of monitors. Appropriate
instrumentation
can limit system e
ects on the monitors. In our asynchronous actor
setting,
direct
interferences from the system to the monitors can be precluded by (
i
)
locating the monitors at process identifiers
not
known to the system (
ii
) preventing the
monitors from communicating these identifiers to the system. These measures inhibit
the system's ability to send messages to the monitors.
A system may also interfere with monitor executions indirectly by
diverging
, i.e.,
infinite internal computation (
ff
-transitions) without external actions. This can prevent
the monitors from executing and thus postpone indefinitely violation detections [25].
In our case, divergence is handled, in part, by the EVM itself, which guarantees fair
executions for concurrent actors [7]. In settings where fair executions may be assumed,
it su
τ
ces to require a weaker property from monitors, reminiscent of the condition in
fair
/
should-testing[26]. Def. 3 states that, for an arbitrary basic action
α
, an actor system
A
satisfies the predicate
should-
if, for
any
sequence of internal actions, there always
exists
an execution that can produce the action
α
; in the case of monitors, the external
should-action is set to a reserved violation-detection action, e.g.,
fail
!.
Definition 3 (Should-
α
=
A
==⇒
B
α
def
α
).
A
⇓
α
==⇒
B
implies
We limit monitoring to
monitorable
systems, where all actors are subject to a moni-
torable modality.
h
)
i
[
e
B
q
]
m
A
≡
(
ν
implies
m
= ◦
This guarantees that (
i
) they can be composed with a tracer actor (
ii
) all the basic actions
produced by the system are recorded as trace entries at the tracer's mailbox.
7
Monitor
correctness is defined for (unmonitored)
basic
systems, satisfying the condition:
7
Due to asynchronous communication, even scoped actors can produce visible actions by send-
ing messages to environment actors.
