Runtime Verification with State Estimation
Runtime Verification with State Estimation
复制标题
使用状态估计进行运行时验证
DOI：
10.1007/978-3-642-29860-8_15
复制
发表时间：
2011
期刊：
影响因子：
2.2
通讯作者：
E. Zadok
中科院分区：
文献类型：
--
作者：
S. Stoller;E. Bartocci;Justin Seyster;R. Grosu;K. Havelund;S. Smolka;E. Zadok
我们介绍了状态估计的运行时验证的概念，并展示了如何应用这个概念来估计当通过抽样减少监控开销时程序运行满足时间属性的概率。在这种情况下，在观察到的程序执行中可能存在间隙，从而使准确的评估具有挑战性。为了处理采样对运行时验证的影响，我们将事件序列视为隐马尔可夫模型（HMM）的观测序列，使用被监控程序的隐马尔可夫模型来“填补”观测序列中由采样引起的间隙，并扩展经典的HMM状态估计前向算法（确定给定观测序列的状态序列的概率），以计算程序执行时满足属性的概率。为了验证我们的方法，我们提出了一个基于火星探测器任务软件的案例研究。算例结果表明，本文算法计算的概率具有较高的预测精度。他们还表明，我们的技术比简单地评估给定观测序列的时间特性而忽略间隙要准确得多。
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.
DOI：
10.1007/978-3-540-72522-0_4
发表时间：
2007
期刊：
--
影响因子：
--
作者：
Clark A
通讯作者：
Clark A