[Zurück]


Vorträge und Posterpräsentationen (mit Tagungsband-Eintrag):

K. Kalajdzic, E. Bartocci, S. Stoller, S. Smolka, R. Grosu:
"Runtime Verification with Particle Filtering";
Vortrag: RV 2013, the Fourth International Conference on Runtime Verification, RENNES, France; 24.09.2013 - 27.09.2013; in: "Proc. of RV 2013, the Fourth International Conference on Runtime Verification", LNCS/Springer, 8174 (2013), ISBN: 978-3-642-40786-4; S. 149 - 166.



Kurzfassung englisch:
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.


"Offizielle" elektronische Version der Publikation (entsprechend ihrem Digital Object Identifier - DOI)
http://dx.doi.org/10.1007/978-3-642-40787-1_9


Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.