NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Back to Results
Runtime Verification with State EstimationWe introduce the concept of Runtime Verification with State Estimation and show how this concept can be applied to estimate theprobability 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.
Document ID
20150006072
Acquisition Source
Jet Propulsion Laboratory
Document Type
Conference Paper
External Source(s)
Authors
Stoller, Scott D.
(Stony Brook Univ. Stony Brook, NY, United States)
Bartocci, Ezio
(Stony Brook Univ. Stony Brook, NY, United States)
Seyster, Justin
(Stony Brook Univ. Stony Brook, NY, United States)
Grosu, Radu
(Stony Brook Univ. Stony Brook, NY, United States)
Havelund, Klaus
(Jet Propulsion Lab., California Inst. of Tech. Pasadena, CA, United States)
Smolka, Scott A.
(Stony Brook Univ. Stony Brook, NY, United States)
Zadok, Erez
(Stony Brook Univ. Stony Brook, NY, United States)
Date Acquired
April 22, 2015
Publication Date
September 27, 2011
Subject Category
Statistics And Probability
Computer Programming And Software
Meeting Information
Meeting: International Conference on Runtime Verification
Location: San Francisco, CA
Country: United States
Start Date: September 27, 2011
End Date: September 30, 2011
Sponsors: California Univ., Jet Propulsion Lab., California Inst. of Tech.
Funding Number(s)
CONTRACT_GRANT: NSF-CCF-1018459
CONTRACT_GRANT: AFOSR-FA9550-09-1-0481
CONTRACT_GRANT: NSF-CCF-0926190
CONTRACT_GRANT: ONR-N00014-07-1-0928
CONTRACT_GRANT: NSF-CNS-0831298
Distribution Limits
Public
Copyright
Other
Keywords
sampling
makov models
runtime verification
temporal logic

Available Downloads

There are no available downloads for this record.
No Preview Available