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.
|