Information Technology Reference
In-Depth Information
We have constructed a tool [29] that implements the monitor synthesis of Def. 6:
given an sHML formula it generates a monitor that can be instrumented with minimal
changes to the system code, as discussed earlier in Sec. 4. The performance of our
synthesised monitor was evaluated through a simulated server that launches individual
workers to handle a series of requests from individual clients; we also injected faults
making certain workers non-deterministically behave erratically. We synthesised mon-
itors to check that each worker observes the
no-duplicate-reply
property from Ex. 4:
[wrk?req]
max
(
X
[clnt!rply][wrk?req]
X
)
ϕ
wrkr
,
[clnt!rply][clnt!rply]
ff
∧
and calculated the overheads incurred for varying number of client requests (i.e., con-
current workers); we also compared this with the performance a monitor that checks for
property violations in sequential fashion. Tests were carried out on an Intel Core i7 pro-
cessor with 8GB of RAM, running Microsoft Windows 8 and EVM version R15B02.
The result, summarised in the table below, show that our synthesised concurrent moni-
toring yields acceptable overheads that are consistently lower than those of a sequential
monitor. We conjecture that this discrepancy can be increased further when monitoring
for recursive properties with longer chains of necessity formulas.
Unmonitored
Sequential
Concurrent
No of. Reqs.
Time
(
μ
s)
Time
(
μ
s)
Ovhd
(%)
Time
(
μ
s)
Ovhd.
(%)
Improv.
(%)
250
117.813
121.667
3.27
118.293
0.40
2.86
350
185.232
202.500
9.32
194.793
5.16
4.16
450
237.606
248.333
4.51
242.380
2.01
2.51
550
286.461
319.167
11.42
308.853
7.82
3.60
650
345.543
372.232
7.72
354.333
2.54
5.18
6
Proving Correctness
The preliminary results obtained in Sec. 5 advocate for the feasibility of using concur-
rent monitors. We however still need to show that the monitors synthesised are correct.
Def. 5 allows us to state one of the main results of the paper, Theorem 2.
Theorem 2 (Correctness).
Fo r a l l
ϕ ∈
sHML
,
Mon
(
ϕ
)
is a correct monitor for
ϕ
.
Proving Theorem 2 directly can be an arduous task: for
any
sHML formula, it re-
quires reasoning about
all
the possible execution paths of
any
monitored system in
parallel with the instrumented monitor. We propose a formal technique for alleviating
the task of ascertaining the monitor correctness of Def. 5 by teasing apart
three
separate
(weaker) monitor-conditions: they are referred to as
Violation Detectability
,
Detection
Preservation
and
Monitor Separability
. These conditions are important properties in
their own right— for instance, Detection Preservation requires the monitor to behave
deterministically
wrt. violation detections. Moreover, the three conditions pose advan-
tages to the checking of monitor correctness: since these conditions are independent to
one another, they can be checked in parallel by distinct analysing entities; alternatively,
the conditions that are inexpensive to check may be carried out before the more expen-
sive ones, thus acting as vetting phases that abort early and keep the analysis cost to a