Report on A Formally-Founded Model-Based Approach to Engineer Self-Adaptive Systems

TL;DR

This paper presents ActivFORMS, a formal, model-based framework for engineering self-adaptive systems that uses verified models and statistical analysis to enable runtime adaptation and goal updates, validated on an IoT security monitoring application.

Contribution

It introduces ActivFORMS, a novel approach combining formal models, runtime verification, and dynamic goal updates for self-adaptive systems.

Findings

Validated on an IoT security monitoring system

Supports on-the-fly adaptation goal changes

Uses formal verification for reliable self-adaptation

Abstract

Self-adaptive systems manage themselves to deal with uncertainties that can only be resolved during operation. A common approach to realize self-adaptation is by adding a feedback loop to the system that monitors the system and adapts it to realize a set of adaptation goals. ActivFORMS (Active FORmal Models for Self-adaptation) provides an end-to-end approach for engineering self-adaptive systems. ActivFORMS relies on feedback loops that consists of formally verified models that are directly deployed and executed at runtime to realize self-adaptation. At runtime, the approach relies on statistical verification techniques that allow efficient analysis of the possible options for adaptation. Further, ActivFORMS supports on-the-fly changes of adaptation goals and updates of the verified models to to meet the new goals. ActivFORMSi provides a tool-supported instance of ActivFORMS. The approach has been validates using an IoT application for building security monitoring. This report provides complementary material to the paper ``ActivFORMS: A Formally-Founded Model-Based Approach to Engineer Self-Adaptive Systems'' [Weyns and Iftikhar 2019].