ActivFORMS：一种基于模型的自适应系统设计方法
ActivFORMS: A Formally-Founded Model-Based Approach to Engineer Self-Adaptive Systems
摘要：
自适应为计算系统配备了一个反馈回路，使其能够处理由操作期间的不确定性引起的变化，例如资源可用性的变化和工作负载的波动。为了确保系统符合适应目标，最近的研究表明，在运行时使用正式的技术。然而，现有的方法有三个限制，影响他们的实际适用性：（i）他们忽略了反馈回路的行为的正确性，（ii）他们依赖于在运行时的穷举验证，以选择适应选项，以实现适应目标，这是时间和资源的要求，以及（iii）他们提供有限的或没有支持，在运行时改变适应目标。为了解决这些缺点，我们提出了ActivFORMS（自适应主动形式模型）。ActivFORMS为工程自适应系统提供了一种端到端的方法，跨越反馈循环生存周期的四个主要阶段：设计，部署，运行时适应和进化。我们还提出了ActivFORMS-ta，一个工具支持的ActivFORMS实例，利用定时自动机模型和统计模型检验在运行时。我们使用部署在鲁汶的物联网应用程序来验证研究结果。实验结果表明，ActivFORMS支持反馈环行为的正确性，以有效的方式实现自适应目标，并支持在运行时改变自适应目标。
英文摘要：
Self-adaptation equips a computing system with a feedback loop that enables it dealing with change caused by uncertainties during operation, such as changing availability of resources and fluctuating workloads. To ensure that the system complies with the adaptation goals, recent research suggests the use of formal techniques at runtime. Yet, existing approaches have three limitations that affect their practical applicability: (i) they ignore correctness of the behavior of the feedback loop, (ii) they rely on exhaustive verification at runtime to select adaptation options to realize the adaptation goals, which is time and resource demanding, and (iii) they provide limited or no support for changing adaptation goals at runtime. To tackle these shortcomings, we present ActivFORMS (Active FORmal Models for Self-adaptation). ActivFORMS contributes an end-to-end approach for engineering self-adaptive systems, spanning four main stages of the life cycle of a feedback loop: design, deployment, runtime adaptation, and evolution. We also present ActivFORMS-ta, a tool-supported instance of ActivFORMS that leverages timed automata models and statistical model checking at runtime. We validate the research results using an IoT application for building security monitoring that is deployed in Leuven. The experimental results demonstrate that ActivFORMS supports correctness of the behavior of the feedback loop, achieves the adaptation goals in an efficient way, and supports changing adaptation goals at runtime.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
