Information Technology Reference
In-Depth Information
Runtime Verification with Particle Filtering
Kenan Kalajdzic 1 , Ezio Bartocci 1 , Scott A. Smolka 2 ,
Scott D. Stoller 2 , and Radu Grosu 1 , 2
1
Faculty of Informatics, Vienna University of Technology, Austria
2
Department of Computer Science, Stony Brook University, USA
Abstract. 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 pro-
gram 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 for-
malization of 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 mon-
itor state after gaps.
We estimate the internal state of the DBN using particle filtering (PF) with
sequential importance resampling (SIR). PF uses a collection of conceptual par-
ticles (random samples) to estimate the probability distribution for the system's
current state: the probability of a state is given by the sum of the importance
weights of 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; particles are then redistributed among the states that best predicted
the current observation. SIR exploits the DBN structure and the current observa-
tion to reduce the variance of the PF and increase its performance.
We experimentally compare the overhead and accuracy of our RVPF algorithm
with two previous approaches to runtime verification with state estimation: an
exact algorithm based on the forward algorithm for HMMs, and an approximate
version of that algorithm, which uses precomputation to reduce runtime overhead.
Our results confim RVPF's versatility, showing how it can be used to control the
tradeoff between execution time and memory usage while, at the same time, being
the most accurate of the three algorithms.
1
Introduction
Runtime verification does not come for free. It introduces runtime overhead, thereby
altering the timing-related behavior of the program under scrutiny. In applications with
realtime constraints, overhead control may be necessary to reduce overhead to an ac-
ceptable level.
In previous work [5], we introduced Software Monitoring with Controllable Over-
head (SMCO), an overhead-control technique that selectively turns monitoring on and
 
Search WWH ::




Custom Search