Information Technology Reference
In-Depth Information
importance resampling
(SIR). The resampling step (which is a performance bottleneck)
does not have to be performed in each round, and the particles are advanced to their
successor states by sampling from the HMM's transition probability distribution
condi-
tioned by
the current observation. While this conditional probability distribution cannot
be computed in general, it can be computed for HMMs.
To handle gaps, we extend PF in a manner that is consistent with the one we devised
for the forward algorithm: as long as gaps are the only observations, the particles are
advanced to their successor states by sampling from the HMM's transition probability
distribution conditioned on the most probable output event. Such output events are cho-
sen by sampling from the output probability distribution of the HMM conditioned on
the previous HMM state. These events are used to drive the DFA transitions.
In contrast to our previous work [10,1], we model the HMM, the DFA, and their
composition in a more elegant and succinct way as a dynamic Bayesian network (DBN).
This allows us to properly formalize a new kind of event, called
peek events
, which are
inexpensive observations of part of the program state. In many applications, program
states and monitor states are correlated, and hence peek events can be used to narrow
down the possible states of the monitor DFA. We use peek events at the end of moni-
toring gaps to refocus the HMM and DFA states. Our combination of these two kinds
of observations, program events and peek events, is akin to
sensor fusion
in robotics.
Adjusting the number of particles used by RVPF provides a versatile way to tune the
memory requirements, runtime overhead, and prediction accuracy. With larger numbers
of gaps, the particles get more widely dispersed in the state space, and more particles are
needed to cover all of the interesting states. To evaluate the performance and accuracy of
RVPF, we implemented it along with our previous two algorithms in C and compared
them through experiments based on the benchmarks used in [1]. Our results confirm
RVPF's versatility. Specifically, we demonstrate in Section 6 that, with the right choice
of the number of particles, RVPF consumes 80-100 times less memory than AP-RVSE
while being twice as fast as RVSE, and the most accurate of the three algorithms.
The rest of the paper is organized as follows. Section 2 provides background. Sec-
tions 3 and 4 define the runtime verification problem we are addressing and system
model, respectively. Section 5 presents the RVPF algorithm. Section 6 describes our
evaluation methodology and the results of our experiments. Section 7 discusses related
work. Section 8 offers concluding remarks and directions for future work.
2
Background
This section provides background information on Bayesian networks, dynamic Bayesian
networks, particle filtering, and runtime verification with state estimation.
A
Bayesian network
is a directed acyclic graph in which each node corresponds to
a (discrete or continuous) random variable. An edge from node
X
to node
Y
indicates
that
X
has a direct influence on
Y
,and
X
is called a
parent
of
Y
.Let
B
be a Bayesian
network over variables
X
1
,...,X
n
. Each
X
i
has a conditional probability distribution
P
(
X
i
|
Parents
(
X
i
)) that quantifies the influence of the parents on the node [7].
The meaning of
B
is a joint distribution over its variables. Let
P
(
x
1
,...,x
n
) abbre-
viate
P
(
X
1
=
x
1
∧···∧
X
n
=
x
n
), i.e., the conjunction of particular assignments
