ActivFORMS: A Formally-Founded Model-Based Approach to Engineer Self-Adaptive Systems
This addresses practical applicability issues for engineers developing self-adaptive systems, though it appears incremental as it builds on existing formal techniques.
The paper tackles limitations in existing formal approaches for self-adaptive systems, such as ignoring feedback loop correctness and inefficient runtime verification, by presenting ActivFORMS, an end-to-end engineering approach that supports correctness, efficient goal achievement, and runtime goal changes, validated with an IoT security monitoring application in Leuven.
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.