Runtime Verification With State Estimation
The authors 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 satisfied 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 validate their approach, they present a case study based on the mission software for a Mars rover. The results of their case study demonstrate high prediction accuracy for the probabilities computed by their algorithm. They also show that their technique is much more accurate than simply evaluating the temporal property on the given observation sequences, ignoring the gaps.