Information Technology Reference
In-Depth Information
level and makes the ILP model outcome highly sensitive to the elementary mon-
itoring costs. Figure 9 shows the monitoring overhead of
fir
under the three
modes of monitoring for different cost configurations. One can observe that when
the sampling period is 10
LSP
, the model correctly chooses ET mode for the
monitoring schemes. However, if we set the sampling period to 20
×
LSP
,then
the ILP model provides a hybrid solution for all three cost configurations. The
proposed hybrid solutions have slightly higher overheads in comparison to ET
mode, but perform as good as TT mode except for two cases in practice. The
reason for this discrepancy lies in the fact that our approach is a heuristic algo-
rithm and, hence, finds suboptimal solutions in some cases. Note, however, that
this discrepancy does not dramatically affect the usefulness of our approach.
×
5 Related Work
In classic runtime verification [21], a system is composed with an external ob-
server, called the monitor. This monitor is normally an automaton synthesized
from a set of properties under which the system is scrutinized. From the logical
and language point of view, runtime verification has mostly been studied in the
context of Linear Temporal Logic (LTL) properties [8,10-12,25] and, in partic-
ular, safety properties [14,22]. Other languages and frameworks have also been
developed for facilitating specification of temporal properties [15,16,27]. [6] con-
sidered runtime verification of
ω
-languages. In [7], the authors address runtime
verification of safety-progress [4,20] properties.
The main focus in the literature of runtime verification is on
event-triggered
monitors [17], where every change in the state of the system triggers the mon-
itor for analysis. Alternatively, in
time-triggered
monitoring [2, 3], the monitor
samples the state of the program under inspection at regular time intervals. The
time-triggered approach involves solving an optimization problem that aims at
minimizing the size of auxiliary memory required so that the monitor can cor-
rectly reconstruct the sequence of program state changes. Several heuristics were
introduced to tackle
Finally, in [13], the authors propose a method to control the overhead of soft-
ware monitoring using control theory for discrete event systems. In this work,
overhead control is achieved by temporarily disabling involvement of monitor,
thus avoiding the overhead to pass a user-defined threshold. Another relevant
work to this line of research is [24], where the authors propose sampling using
state estimation. In particular, they use hidden Markov models to estimate fu-
ture reachable states for deciding whether or not the monitor must sample the
program under inspection. However, the methods in [13] and [24] do not guaran-
tee correct state reconstruction because the monitor is unaware of all program
state changes that may occur between samples.
6Con lu on
In this paper, we concentrated on combining two techniques in the literature of
runtime verification to reduce the overhead: (1) the traditional event-triggered
