Expression Caching for Runtime Verification Based on Parameterized Probabilistic Models
Expression Caching for Runtime Verification Based on Parameterized Probabilistic Models
复制标题
基于参数化概率模型的运行时验证表达式缓存
DOI：
10.1016/j.jss.2019.07.007
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Tatsuhiro Tsuchiya
中科院分区：
文献类型：
--
作者：
Hiroyuki Nakagawa;Hiromu Toyama;Tatsuhiro Tsuchiya
自适应软件系统在运行时改变其行为以适应其环境变化。运行时验证用于检查适应后的行为的正确性，有时使用概率模型检查，因为验证必须处理不确定性。然而，由于概率模型检测通常是计算量大、耗时长的，因此需要一种更有效的验证机制。一种可能的方法是在设计时预先生成一些用于模型检查的表达式，并在运行时简单地通过计算表达式来执行模型检查。这种方法的一个问题是，当环境变化需要更改系统模型时，需要在运行时重新生成这些表达式。为了应对如此重大的变化，我们开发了一种缓存机制来减少运行时的计算时间。为了提高缓存的效率，我们还引入了一种参数化技术。实验结果表明，新的缓存机制的实现大大提高了运行时验证的计算时间。
Self-adaptive software systems change their behaviors to adapt to their environmental changes at runtime. Runtime verification, which checks the correctness of behaviors after adaptation, sometimes uses probabilistic model checking, because the verification has to deal with uncertainty. However, since probabilistic model checking is usually computation intensive and time consuming, a more efficient verification mechanism is desired. A possible approach is to pre-generate some expressions for model checking at design time and execute model checking simply by evaluating the expressions at runtime. A problem with this approach is that when environmental changes require changes of the system model, these expressions need to be re-generated at runtime. In order to cope with such significant changes, we develop a caching mechanism that reduces computational time at runtime. We also introduce a parameterization technique in order to improve the efficiency of caching. The experimental results show that our new implementation of the caching mechanism greatly improves the computational time of runtime verification.