JPL Technical Report Server

Runtime verification with state estimation

Show simple item record

dc.contributor.author Stoller, Scott D.
dc.contributor.author Bartocci, Ezio
dc.contributor.author Seyster, Justin
dc.contributor.author Grosu, Radu
dc.contributor.author Havelund, Klaus
dc.contributor.author Smolka, Scott A.
dc.contributor.author Zadok, Erez
dc.date.accessioned 2013-09-09T15:00:47Z
dc.date.available 2013-09-09T15:00:47Z
dc.date.issued 2011-09-26
dc.identifier.citation 2nd International Conference on Runtime Verification, San Francisco, California, September 27 - 30, 2011 en_US
dc.identifier.clearanceno 11-4131
dc.identifier.uri http://hdl.handle.net/2014/43652
dc.description.abstract 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 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 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 (which determines the probability of a state sequence, given an observation sequence) to compute the probability that the property is satisfied 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. en_US
dc.description.sponsorship NASA/JPL en_US
dc.language.iso en_US en_US
dc.publisher Pasadena, CA : Jet Propulsion Laboratory, National Aeronautics and Space Administration, 2011. en_US
dc.subject runtime verification en_US
dc.subject sampling en_US
dc.subject temporal logic en_US
dc.subject makov models en_US
dc.title Runtime verification with state estimation en_US
dc.type Preprint en_US


Files in this item

This item appears in the following Collection(s)

Show simple item record

Search


Browse

My Account