K. Kalajdzic,E. Bartocci, S. Stoller, S. Smolka, R. Grosu:

"Runtime Verification with Particle Filtering";

Talk: RV 2013, the Fourth International Conference on Runtime Verification, RENNES, France; 2013-09-24 - 2013-09-27; in: "Proc. of RV 2013, the Fourth International Conference on Runtime Verification", LNCS/Springer, 8174 (2013), ISBN: 978-3-642-40786-4; 149 - 166.

We introduce Runtime Verification with Particle Filtering (RVPF),

a powerful and versatile method for controlling the tradeoff between

uncertainty and overhead in runtime verification. Overhead and accuracy

are controlled by adjusting the frequency and duration of

observation gaps, during which program events are not monitored,

and by adjusting the number of particles used in the RVPF algorithm.

We succinctly represent the program model, the program monitor, their

interaction, and their observations as a dynamic Bayesian network (DBN).

Our formulation of RVPF in terms of DBNs is essential for a proper

formalization of {\em peek events}: low-cost observations of

parts of the program state, which are performed probabilistically at

the end of observation gaps. Peek events provide information that our

algorithm uses to reduce the uncertainty in the monitor state after gaps.

%Consequently, we model peek events as partial observations of the

%monitor state.

We estimate the internal state of the DBN using particle filtering (PF)

with sequential importance resampling (SIR). PF uses a collection of

conceptual particles (random samples) to estimate the probability distribution for the

system's current state: the probability of a state is given by the sum

of importance weights of all the particles in that state. After

an observed event, each particle chooses a state transition to execute

by sampling the DBN's joint transition probability distribution;

% I made "joint transition probability distributions" singular. --sas

particles are then redistributed among the states which best predicted

the current observation. SIR exploits the DBN structure and the current

observation to reduce the variance of the PF and increase its performance.

%% Our combination of observations (program events

%% and peek events) can be seen as a type of \emph{sensor fusion}.

We experimentally compare the overhead and accuracy of our new RVPF

algorithm with two previous approaches to state estimation in runtime

verification with overhead control: an exact algorithm based on the forward

algorithm for HMMs, and an approximate version of that algorithm that uses

precomputation to reduce runtime overhead.

Our experiments confim the versatility of particle filtering, which

allows for control of the tradeoff between speed and memory consumption

while being the most accurate of all the three considered algorithms.

http://dx.doi.org/10.1007/978-3-642-40787-1_9

Created from the Publication Database of the Vienna University of Technology.