ActivFORMS: A Model-Based Approach to Engineer Self-Adaptive Systems

Handling change is an increasingly important challenge for software engineers. Our focus is on changes caused by uncertainties in the operating conditions of a system, such as changes in the availability of resources in a highly dynamic environment. To deal with such uncertainties, an external feedback loop system can be added to the system that collects additional data during operation to resolve the uncertainties and adapt the system to achieve particular quality requirements (i.e., adaptation goals); this approach is commonly referred to as self-adaptation. To ensure that the system complies with the adaptation goals, recent research suggests the use of formal techniques at runtime. Existing approaches have three shortcomings that limit their practical applicability: (i) they ignore correctness of the behavior of the feedback loop, (ii) they apply exhaustive verification at runtime to select adaptation options to realize the adaptation goals, which is very 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: (i) provides guarantees for the correct behavior of the feedback loop with respect to a set of correctness properties at design time and preserves the guarantees at runtime by directly executing the verified models of the feedback loop, (ii) guides the adaptation of the system by selecting adaptation options that realize the adaptation goals in an efficient manner using statistical model checking at runtime, and (iii) offers basic support for changing adaptation goals and updating verified models of the feedback loop on-the-fly to meet the new goals. To validate ActivFORMS, we present a tool-supported instance of the approach that we apply to an IoT application for building security monitoring deployed in Leuven.