To accurately make adaptation decisions, a self-adaptive system needs precise means to analyze itself at runtime. To this end, runtime verification can be used in the feedback loop to check that the managed system satisfies its requirements formalized as temporal-logic properties. These requirements, however, may change due to system evolution or uncertainty in the environment, managed system, and requirements themselves. Thus, the properties under investigation by the runtime verification have to be dynamically adapted to represent the changing requirements while preserving the knowledge about requirements satisfaction gathered thus far, all with minimal latency. To address this need, we present a runtime verification approach for self-adaptive systems with changing requirements. Our approach uses property specification patterns to automatically obtain automata with precise semantics that are the basis for runtime verification. The automata can be safely adapted during runtime verification while preserving intermediate verification results to seamlessly reflect requirement changes and enable continuous verification. We evaluate our approach on an Arduino prototype of the Body Sensor Network and the Timescales benchmark. Results show that our approach is over five times faster than the typical approach of redeploying and restarting runtime monitors to reflect requirements changes, while improving the system's trustworthiness by avoiding interruptions of verification.
翻译:为了准确做出自适应决策,自适应系统需要在运行时精确分析自身。为此,可以在反馈循环中使用运行时验证来检查被管理的系统满足其以时间逻辑属性形式规定的要求。然而,这些要求可能会由于系统演化或环境、被管理系统和要求本身的不确定性而发生变化。因此,正在由运行时验证调查的属性必须动态适应以表示变化的要求,同时保留迄今为止收集的有关要求满足的知识,以尽可能地减少延迟。为了应对这一需求,我们提出了一种针对自适应系统动态需求的运行时验证方法。我们的方法使用属性规范模式自动获取带有精确语义的自动机,这是运行时验证的基础。在运行时验证期间,自动机可以安全地适应,同时保留中间验证结果,以无缝反映需求变化并实现连续验证。我们在Body Sensor Network和Timescales基准测试的Arduino原型上评估了我们的方法。结果表明,与反复部署和重新启动运行时监视器以反映要求变化的典型方法相比,我们的方法速度提高了五倍以上,同时通过避免验证中断提高了系统的可信度。