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.
翻译:为准确做出自适应决策,自适应系统需要精确的手段在运行时对其自身进行分析。为此,可在反馈回路中运用运行时验证,以检查被管系统是否满足被形式化为时序逻辑属性的需求。然而,这些需求可能因系统演化或环境、被管系统及需求本身的不确定性而发生变化。因此,运行时验证所研究的属性必须动态调整以表征变化的需求,同时保留迄今收集到的关于需求满足情况的知识,且整个过程需具有最小延迟。为满足这一需求,我们提出了一种适用于具有变化需求的自适应系统的运行时验证方法。该方法利用属性规约模式自动获取具有精确语义的自动机,作为运行时验证的基础。在运行时验证过程中,这些自动机可被安全地调整,同时保留中间验证结果,以无缝反映需求变化并实现持续验证。我们基于Arduino平台的身体传感器网络原型与Timescales基准测试对所提方法进行了评估。结果表明,相比重新部署并重启运行时监测器以反映需求变化的典型方法,我们的方法速度快了五倍以上,同时通过避免验证中断提升了系统的可信度。