Stoller/Bartocci/Seyster/Grosu/Havelund/Smolka/Zadok
## Aspect-Oriented Instrumentation with GCC.*

*S.D. Stoller, E. Bartocci, J. Seyster, R. Grosu, K. Havelund, S.A. Smolka, and E. Zadok*
We introduce the concept of *Runtime Verification with State
Estimation* and show how this concept can be applied to estimate the
probability that a temporal property is satised by a run of a program
when monitoring overhead is reduced by sampling. In such situations,
there may be gaps in the observed program executions, thus making accurate
estimation challenging. To deal with the effects of sampling on
runtime verification, we view event sequences as observation sequences
of a Hidden Markov Model (HMM), use an HMM model of the monitored
program to "fill-in" sampling-induced gaps in observation sequences, and
extend the classic forward algorithm for HMM state estimation (determine
the probability of a state sequence, given an observation sequence)
to compute the probability that the property is satised by an execution
of the program. To validate our approach, we present a case study based
on the mission software for a Mars rover. The results of our case study
demonstrate high prediction accuracy for the probabilities computed by
our algorithm. They also show that our technique is much more accurate
than simply evaluating the temporal property on the given observation
sequences, ignoring the gaps.

*
In Proc. of RV'11, the 2nd International Conference on Runtime Verification,
San Francisco, November, 2011, Springer LNCS.
*

*This work was supported by NSF Expeditions Award CNS-09-26190, the NSF
CSR-AES05-09230 Award and the AFOSR FA-0550-09-1-0481 Award.