Information Technology Reference
In-Depth Information
Organization.
The rest of the paper is organized as follows. Section 2 describes
the concepts of ETRV and TTRV. Section 3 introduces the HyRV optimization
problem. We analyze the results of our experiments in Section 4. Section 5 dis-
cusses the related work. Finally, in Section 6, we make concluding remarks and
discuss future work.
2 Background
Let
P
be a program under inspection and Π be a logical property (e.g., in LTL),
where
P
is expected to satisfy Π. Let
V
Π
denote the set of variables that par-
ticipate in Π. In
event-triggered runtime verification
(ETRV), the instrumented
version of
P
invokes the monitor to evaluate Π whenever the value of some
variable in
V
Π
changes.
In
time-triggered runtime verification
(TTRV) [2, 3], a monitor
samples
the
value of variables in
V
Π
periodically and evaluates Π. Accurate reconstruction of
states of
P
between two consecutive samples is the main challenge in using this
mechanism; e.g., if the value of a variable in
V
Π
changes more than once between
two samples, then the monitor may fail to detect violations of Π. TTRV usually
leverages control-flow analysis to reconstruct the states of
P
.
To ensure that the behaviour of a time-triggered monitor is correct, the mon-
itor must sample at a 'safe' rate determined by statically analyzing
P
's control-
flow graph:
Definition 1.
The
control-flow graph
(CFG) of a program
P
is a weighted di-
rected simple graph CFG
P
=
V,v
0
,A,w,v
f
,where:
-
V
:isasetof
vertices
, each representing a basic block of
P
. Each basic block
consists of a sequence of instructions in
P
.
-
v
0
:isthe
initial vertex
with in-degree 0, which represents the initial basic
block of
P
.
-
A
:isasetof
arcs (
u,v
)
,where
u,v
V
.Anarc
(
u,v
)
exists in
A
,ifand
only if the execution of basic block
u
immediately leads to the execution of
basic block
v
.
-
w
:isafunction
w
:
A
∈
, which defines a
weight
for each arc in
A
.The
weight of an arc is the
best-case execution time
(BCET) of the source basic
block.
-
v
f
: is a dummy vertex which acts as final vertex. It has incoming arcs from
all actual final vertices. This helps in simplifying analysis by allowing us to
easily consider weight of final vertices.
→
N
For example, consider the C program in Figure 2 [2]. Figure 3(a) shows the
resulting CFG assuming that the BCET of each line of code is one time unit.
Vertices of the graph in Figure 3 list the corresponding line numbers of the C
program in Figure 2.
To identify the
sampling period
that a monitor can accurately reconstruct
program states between two samples, we modify
CFG
P
as follows:
