ActivFORMS: Active Formal Models for Self-Adaptation

Home - MAPE-K Templates


    Self-adaptation is typically realized with a feedback loop that consists of monitor, analysis, plan, and execution functions. To guarantee that the adaptation goals are met at runtime, Active FORmal Model for Self-adaptation (ActivFORMS) uses formally verified models of the feedback loop. These models are directly executed at runtime by a virtual machine to realize adaptation. We use timed automata as modeling formalism and Uppaal as design tool. ActivFORMS enables continues verification of adaptation goals at runtime as well as dynamic updates of the formal models to support unanticipated changes, assuring that the verified system goals are met.