Information Technology Reference
In-Depth Information
h
)
i
[
e
B
q
]
m
A
≡
(
ν
implies
m
= •
which are instrumented to execute in parallel with the monitor. Our instrumentation
is defined through the operation
, Def. 4, converting basic systems to monitorable
ones using
trace/2
and
set on spawn
Erlang commands [7]; see Lemma 1. Im-
portantly, instrumentation does not a
−
ff
ect the visible behaviour of a basic system; see
Lemma 2.
Definition 4 (Instrumentation).
−
:: Actr
→
Actr
is defined inductively as:
q
]
m
def
=
q
]
◦
def
=
def
=
i
[
e
i
[
e
B
C
B
C
(
ν
i
)
B
(
ν
i
)
B
Lemma 1.
If A is a basic system then
A
is monitorable.
Lemma 2.
For all basic actors A where i
fId(
A
)
:
⎩
i
)
q
]
∗
i
)
]
∗
j
!
v
−−−→
(
ν
A
i
[
e
(
ν
B
i
[
e
q
:
{
sd
,
j
,
v
}
if
α=
j
!
v
A
α
i
)
q
]
∗
i
)
]
∗
j
?
v
−−−−→
−−→
Bi
ff
(
ν
A
i
[
e
(
ν
B
i
[
e
q
:
{
rv
,
j
,
v
}
if
α=
j
?
v
i
)
q
]
∗
τ
i
)
q
]
∗
(
ν
A
i
[
e
−−→
(
ν
B
i
[
e
if
α=τ
We are now in a position to state monitor correctness, for some predefined violation-
detection monitor action
fail
!, Def. 5; in what follows,
fail
isalwaysassumedtobe
fresh. We restrict our definition to expressions
e
located at a fresh scoped location
i
(not used by the system, i.e.,
i
; expression
e
may
then spawn concurrent submonitors while executing. The definition can be extended to
generic concurrent monitors, i.e., multiple expressions, in straightforward fashion.
fId(
A
)) with an empty mailbox,
Definition 5 (Correctness).
e
∈
Exp
is a correct monitor for
ϕ ∈
sHML
i
ff
for any
∈
Act
\{
fail
!
}
∗
:
basic actors A
∈
Actr
,i
fId(
A
)
, and execution traces s
i
)
i
[
e
]
∗
A
⇓
fail
!
s
==⇒
(
ν
A
B
implies
,
s
|=
v
ϕ
i
ff
B
Def. 5 states that
e
correctly monitors property
ϕ
whenever, for any trace of environ-
i
)
]
∗
, yielding system
B
,if
ment interactions,
s
, of a monitored system, (
ν
A
i
[
e
s
leads
A
to a violation of
ϕ
, then system
B
should always detect it, and viceversa.
5
Automated Monitor Synthesis
We define a translation from sHML formulas to Erlang
monitors
that asynchronously
analyse a system and flag an alert whenever they detect violations by the current sys-
tem execution (for the respective sHML formula). This translation describes the core
algorithm for a tool automating monitor synthesis from sHML formulas [29].
Despite its relative simplicity, the sHML provides opportunities to perform con-
current monitoring. The most obvious case is the translation of conjunction formulas,
ϕ
1
∧ϕ
2
, whereby the resulting code needs to check
both
sub-formulas
ϕ
1
and
ϕ
2
so as to
