Information Technology Reference
In-Depth Information
minimum. More importantly though, the three conditions together imply our original
monitor-correctness criteria.
The first sub-property is
Violation Detectability
, Lemma 3, guaranteeing that every
violating trace
s
of formula
is detectable by the respective synthesised monitor,
10
(the
only-if
case) and that there are no false detections (the
if
case). This property is easier
to verify than Theorem 2 since it requires us to consider the execution of the monitor in
isolation and, more importantly, requires us to verify the
existence of an execution path
that detects the violation; concurrent monitors typically have multiple execution paths.
ϕ
s
=⇒
Lemma 3 (Violation Detectability).
For basic A
∈
Actr
and i
fId(
A
)
,A
implies:
fail
!
===⇒
tr(
s
)]
∗
A
,
s
|=
v
ϕ
i
ff
i
[
Mon
(
ϕ
)
Detection Preservation (Lemma 4), the second sub-property, is not concerned with
relating detections to actual violations. Instead it guarantees that if a monitor can po-
tentially detect a violation, further reductions do not exclude the possibility of this de-
tection. In the case where monitors always have a finite reduction wrt. their mailbox
contents (as it turns out to be the case for monitors synthesised by Def. 6) this condition
guarantees that the monitor will deterministically detect violations.
Val
∗
Lemma 4 (Detection Preservation).
Fo r a l l
ϕ∈
sHML
,q
∈
i
[
Mon
(
B
fail
!
===⇒
fail
!
===⇒
q
]
∗
q
]
∗
==⇒
ϕ
)
and i
[
Mon
(
ϕ
)
implies
B
The third sub-property is Separability, Lemma 5, which implies that the behaviour of
a (monitored) system
is independent of
the monitor and, dually, the behaviour of the
monitor depends,
at most
, on the trace generated by the system.
Lemma 5 (Monitor Separability).
For all basic A
∈
Actr
,
i
fId(
A
)
,ϕ∈
sHML
,
and
∈
Act
\{
}
∗
,
s
fail
!
i
)
)]
∗
s
==⇒
B
,
B
s.t.
(
ν
A
i
[
Mon
(
ϕ
B implies
∃
i
)
B
B
s
=⇒
A
s.t.
B
=
A
tr(
s
)]
∗
==⇒
B
≡
ν
ϕ
B
(
and
A
and
i
[
Mon
(
)
These three properties su
ce to show monitor correctness.
Theorem 2
(Correctness).
Fo r a l l
ϕ ∈
sHML
,
Mon
(
ϕ
)
is a correct monitor for
ϕ
.
Proof.
According to Def. 5 we have to show:
i
)
)]
∗
A
⇓
fail
!
s
==⇒
B
(
ν
A
i
[
Mon
(
ϕ
,
s
|=
v
ϕ
i
ff
B
implies
For the
only-if
case, we assume
i
)
A
)]
∗
s
==⇒
B
(
ν
i
[
Mon
(
ϕ
(3)
A
,
s
|=
v
ϕ
(4)
10
We elevate tr to basic action sequences
s
in pointwise fashion, tr(
s
), where tr(
)
=
.
