Adaptive Runtime Verification
Adaptive Runtime Verification
复制标题
自适应运行时验证
DOI：
10.1007/978-3-642-35632-2_18
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Justin Seyster
中科院分区：
文献类型：
--
作者：
E. Bartocci;R. Grosu;A. Karmarkar;S. Smolka;S. Stoller;E. Zadok;Justin Seyster
我们提出了自适应验证（ARV），一种新的方法来运行时验证，其中开销控制，运行时验证与状态估计，预测分析协同结合。开销控制通过根据需要启用和禁用每个监视器实例的事件监视，将运行时验证的开销保持在指定的目标级别。在ARV中，基于被监控系统的概率模型的预测分析被用于估计每个监控实例在不久的将来违反给定时间属性的可能性，并且这些关键性级别被馈送到开销控制器，开销控制器将目标开销的较大部分分配给具有较高关键性的监控实例，从而增加违规检测的概率。由于开销控制会导致监视器错过事件，因此我们使用带有状态估计的验证验证（RVSE）来估计不完全监视的运行满足属性的概率。ARV框架的一个关键方面是RVSE的新算法，该算法提前执行计算，大大减少了RVSE的运行时开销，但代价是引入了一些近似误差。我们证明了实用的ARV上的一个重要的案例研究，涉及运行时监测并发错误的Linux内核。
We present Adaptive Runtime Verification (ARV), a new approach to runtime verification in which overhead control, runtime verification with state estimation, and predictive analysis are synergistically combined. Overhead control maintains the overhead of runtime verification at a specified target level, by enabling and disabling monitoring of events for each monitor instance as needed. In ARV, predictive analysis based on a probabilistic model of the monitored system is used to estimate how likely each monitor instance is to violate a given temporal property in the near future, and these criticality levels are fed to the overhead controllers, which allocate a larger fraction of the target overhead to monitor instances with higher criticality, thereby increasing the probability of violation detection. Since overhead control causes the monitor to miss events, we use Runtime Verification with State Estimation (RVSE) to estimate the probability that a property is satisfied by an incompletely monitored run. A key aspect of the ARV framework is a new algorithm for RVSE that performs the calculations in advance, dramatically reducing the runtime overhead of RVSE, at the cost of introducing some approximation error. We demonstrate the utility of ARV on a significant case study involving runtime monitoring of concurrency errors in the Linux kernel.
DOI：
10.1007/978-3-540-72522-0_4
发表时间：
2007
期刊：
--
影响因子：
--
作者：
Clark A
通讯作者：
Clark A