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

arXiv: https://arxiv.org/abs/1908.11179 · HTML: https://mlsanity.com/paper/1908.11179/

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 29 Aug 2019.

## Built on by (most cited first, 5 of 5)

- [Generative AI for Self-Adaptive Systems: State of the Art and Research Roadmap](https://mlsanity.com/paper/2512.04680/) (2025)
- [The Vision of Self-Evolving Computing Systems](https://mlsanity.com/paper/2204.06825/) (2022)
- [Deep Learning for Effective and Efficient Reduction of Large Adaptation Spaces in Self-Adaptive Systems](https://mlsanity.com/paper/2204.06254/) (2022)
- [Dealing with Drift of Adaptation Spaces in Learning-based Self-Adaptive Systems using Lifelong Self-Adaptation](https://mlsanity.com/paper/2211.02658/) (2022)
- [Awareness requirement and performance management for adaptive systems: a survey](https://mlsanity.com/paper/2302.05518/) (2023)

## Abstract (arXiv)

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.