Information Technology Reference
In-Depth Information
⇓
fail
!
, by Def. 3 we also assume
B
==⇒
B
, for arbitrary
B
, and then be
To sh ow
B
fail
!
==⇒
required to prove that
B
B
and Lemma 5 we know
.From(3),
B
==⇒
i
)
B
B
B
,
B
s.t.
B
≡
∃
(
ν
(5)
s
==⇒
A
for some
A
where
A
=
B
A
(6)
tr(
s
)]
∗
===⇒
B
ϕ
i
[
Mon
(
)
(7)
fail
!
==⇒
tr(
s
)]
∗
ϕ
From (6), (4) and Lemma 3 we obtain
i
[
Mon
(
)
, and from (7) and
fail
!
==⇒
Lemma 4 we get
B
. Hence, by (5), and standard transition rules for parallel
composition and scoping, Par and Scp, we can reconstruct
B
fail
!
===⇒
, as required.
For the
if
case we assume:
i
)
)]
∗
s
==⇒
B
ν
ϕ
(
A
i
[
Mon
(
(8)
⇓
fail
!
B
(9)
fail
!
===⇒
,
|=
v
ϕ
andhavetoprove
A
s
. From (9) we know
B
. Together with (8) this implies
∃
B
s.t. (
ν
i
)
A
i
[
Mon
(
ϕ
)]
∗
s
==⇒
B
fail
!
−−−→
(10)
From Lemma 5 and (10) we obtain
i
)
B
B
B
,
B
s.t.
B
=
∃
(
ν
(11)
s
==⇒
A
for some
A
where
A
=
B
A
(12)
tr(
s
)]
∗
==⇒
B
i
[
Mon
(
ϕ
)
(13)
fail
!
−−→
From (10), (11) and the freshness of
fail
!to
A
we deduce that
B
, and subsequently,
fail
!
==⇒
by (13), we get
i
mtr
[
Mon
(
ϕ
)
tr(
s
)]
. Therefore, by (12) and Lemma 3 we obtain
A
,
s
|=
v
ϕ
, as required.
7Con lu ion
We have studied a more intensional notion of correctness for monitor synthesis in a con-
current online setting; we worked close to the actual implementation level of abstraction
so as to enhance our confidence in the correctness of our instrumented monitors. More
precisely, we have identified a number of additional issues raised when proving mon-
itor correctness in this concurrent setting, illustrating them through a case study that
builds a tool [29] automating monitor synthesis from a reactive property logic (sHML)
to asynchronous monitors in a concurrent language (Erlang). The specific contributions
of the paper, in order of importance, are:
1.
A novel formal
definition of monitor correctness
, Def. 5, dealing with issues such
as system non-determinism and system interference.
