Skip to content The Open University

ActivFORMS: Active Formal Models for Self-Adaptive Systems

An important challenge for self-adaptive systems is to provide evidence that the system goals are satisfied during operation, regarding the uncertainty of changes that may affect the system, its environment or its goals. To provide such evidence, state of the art approaches propose to equip the feedback loop with formal models of the managed system, the context in which it executes and its goals (or parts of these). These models are updated at runtime to handle uncertainties and support decision making for adaptations. However, existing approaches do not provide guarantees about the behavior of the adaptation functions themselves, which may ruin the adaptation capabilities. Furthermore, the focus is mainly on parametric uncertainty (e.g., likelihood of faults, service availability), but not on structural uncertainty (e.g., adding new goals), which refer to unanticipated changes that typically require dynamic updates, including updates of the feedback loop. In this talk, we introduce Active FORmal Model for Self-adaptation (ActivFORMS) that uses a formal model of the complete feedback loop. This model is directly executed at runtime by a virtual machine to realize self-adaptation. ActivFORMS assures that the verified system goals are guaranteed at runtime, and enables runtime updates of the formal model to support unanticipated changes. We show how we have used ActivFORMS for different adaptation scenarios in a small-scale robotic system.