MAPE-K Templates

Home - ActivFORMS


  Introduction

    Supporting material for the submitted article MAPE-K Formal Templates to Rigorously Design Behaviors for Self-Adaptive Systems is available here.
    Designing software systems that have to deal with dynamic operating conditions, such as changing availability of resources and faults that are difficult to predict, is complex. A promising approach to handle such dynamics is self-adaptation that is realized by a feedback loop. To provide evidence that the system goals are satisfied, regarding the changing conditions, state of the art advocates the use of formal methods. Applying these methods requires accurate specifications of both the models of the self-adaptive system and properties to verify whether the system fulfills its goals. However, little research has been done on consolidating design knowledge of models and properties for self-adaptive systems. To support designers, we derived a set of reusable templates for modeling feedback loops for self-adaptive systems based on the MAPE-K reference model (Monotor-Analyse-Plan-Execute-Knowledge). The templates were derived from our expertise with developing a family of self-adaptive systems. The reusable templates comprise: (1) behavior templates that can be used to model the concrete components of a feedback loop (using networks of timed automata), and (2) specification properties that can be instantiated to support verification of the correctness of the adaptation behaviors (using timed computation tree logic). We provide concrete instances of the reusable templates for a mobile learning application and a robot application.
    The templates are derived from a number of applications that represent a family of systems for which the templates are applicable; example applications are presented at FOCLASA 2012 and SEAMS 2013. This family of systems has the following characteristics:
    • Systems comprise software deployed on distributed nodes;
    • The nodes have an explicit position in the environment (and may be mobile);
    • The system has continual communication access;
    • Dynamics in the system and the environment are orders of magnitude lower than the speed of communication and the execution of the software.
    We study self-adaptation to realize robustness (i.e., the system deals autonomously with particular types of faults) and openness (the system deals autonomously with parts that come and go dynamically). To that end, local feedback loops can observe local managed systems and their execution context and adapt the managed systems by adding and removing resources. Resources are abstractly defined and refer to any type of controllable feature of the managed system, such as components, functions, variables, devices, etc.

  Behavior Templates

    We follow the following color conventions for the description of the behavior templates.

    • States of behaviors are annotated in red.
    • Invariants that need to be satisfied in certain states are annotated in purple.
    • Conditions to enable firing of transitions between states are annotated in green.
    • Signals used for communication between behaviors are annotated dark blue.
    • Functions associated with behaviors are annotated in light blue.

      Monitor

    Fig. 1: Event triggered Monitor template

      A Monitor behavior collects information from the managed system and possibly the environment to update the Knowledge of the feedback loop. Before updating the Knowledge, the Monitor behavior may preprocess the collected data. Examples of preprocessing are standardization of data, filtering, data aggregation, etc.

      We provide Monitor behaviors both with event (top) and time triggering (bottom). Monitor resides in the Waiting state until it is triggered to act. An event triggered Monitor is activated by a probe (either from the managed system or the environment) via the Monitor[Node ID]? signal. A time triggered Monitor periodically (t==Period) activates a probe via monitor(). If necessary, the new collected data is preprocessed (if isPreprocessingRequired() then preprocess()). Then the Knowledge is updated (updateKnowledge()). Finally, the Analyze behavior is notified about the update (Analyze[Node ID]! from the NewChange state). This latter triggering is optional, as the Analyze behavior may use time triggering.


    Fig. 2: Time triggered Monitor template
     

      Analyze

    Fig. 3: Event triggered Analyze template

      The Analyze behavior is responsible to determine whether adaptation actions are required. To that end, the Analyze behavior matches the required resources with the resources in use, taking into account the current context and working data. Analysis can result in three primary conclusions. The current situation is Satisfied when the managed system possesses the resources it requires to realize its goals. The situation is Undersatisfied when the system lacks resources, and Oversatisfied when the system has redundant resources. We provide behavior templates for an analyze behavior with event triggering (Analyze[Node ID]?) and time triggering (t==Period). To perform analysis, the Analysis behavior collects the required knowledge (getRequired(), getUsed(), and getContext(), getWorking-Data()) and then matches resources (matchResources()). The results of the analysis are then communicated to the Plan behavior (Plan OverSatisfied[Node ID]!,Plan Satisfied[Node ID]!, Plan UnSatisfied[Node ID]!). Analysis interacts with Plan through signals, but this is optional.


    Fig. 4: Time triggered Analyze template
     

      Plan

    Fig. 5: Event triggered Plan template

      The Plan behavior is responsible for planning mitigation actions when needed to bring the managed system in a desired state (i.e. Satisfied). There are two cases that require planning: either there is a need to add resources (i.e., the system state is in an unsatisfied situation), or resources may be released (when the system is in an oversatisfied state). We present two reusable templates for a Plan behavior. With time triggering, the planner periodically checks what it needs to do (x==planToDo() condition), and creates an appropriate plan when needed (ReleaseResource or AddResource).

      Planning the release of resources is specified in the left part of the figures of the Plan behavior (releaseResource(dispensible_resource)). In case, a resource is ready for release, a plan is generated, added to Knowledge and Execute is informed. In case no resource is ready for release, Plan periodically re-checks. Planning can be interrupted if conditions change and adaptation is no longer required (satisfied == planToDo() or add == planToDo()). Planning the addition of resources is specified in the right part of the figure findResource(). If Plan finds a suitable resource (found_resource != NONE) it generates a plan, adds it to the Knowledge, and communicates with Execute. Otherwise, Plan rechecks periodically to see whether a resource is available. As for releasing resources, planning the addition of a resource can be interrupted when adaptation is no longer required.


    Fig. 6: Time triggered Plan template
     

      Execute

    Fig. 7: Event triggered Execute template

      The Execute behavior is responsible of executing adaptation plans. Plans an contain multiple actions to be invoked to the managed system. We provide two reusable templates for the Execute behavior, respective with time and event triggering. The left part of the figures with the templates specify the execution of plans to release resources. Actions are only executed when the managed system is ready for it isSystemReadyToTakeAction()). Actions are executed sequentially by invoking an effector ( invokeNextAction()). When the complete plan is executed, the behavior returns to wait for the next plan to be executed (PlanCompleted).

    Fig. 8: Time triggered Execute template
     

  Properties

    Adaptation Goal Specification Property

    The adaptation goal specification property allows to verify when the self-adaptative system requires adaptation, eventually the adaptation will be realized by the MAPE-K loop.

    P1: Analyze(X).Unsatisfied --> Analyze(X).Satisfied || Analyze(X).Oversatisfied

    P1 defines when an Analyse behavior at node X detects that the managed system is in an unsatisfied state, the MAPE behaviors will eventually adapt the managed system bringing it in the satisfied or oversatisfied state. Property P1 is based on the assumption that eventually resources will become available to realize the adaptation goal.

    Intra-Behavior Specification Properties

    Intra-behavior properties allow verification of properties of individual MAPE behaviors, independently of the other MAPE behaviors.

    P2: ConcernKnowledge[X].required_resources > ManagedSystemKnowledge[X].used_resources --> Analyze(X).Unsatisfied
    P3: Plan(X).AddResource --> Plan(X).Satisfied
    P4: Plan(X).ReleaseResource --> Plan(X).Satisfied
    P5: Execute(X).ExecuteAdd --> Execute(X).PlanCompleted
    P6: Execute(X).ExecuteRelease --> Execute(X).PlanCompleted

    P2 defines that when resources used by the managed system are insufficient according the requirements of the Knowledge, the Analyze behavior will eventually detect this unsatisfied situation. The greater than symbol is an abstract operator to check whether the used resources satisfy the required resources, and needs to be instantiated for the domain at hand. Intra-process property verification becomes particularly interesting for complex behaviors. E.g., it is important to verify that the Plan creates adequate plans on how the managed system should be adapted. P3 and P4 are two specification properties for a Plan behavior that allow to verify whether adding (P3) and releasing a resource (P4) from the managed system leads to a Satisfied state. P5 and P6 specify properties for an Execute behavior that allow to verify whether the plan for adding a resource (P5) and releasing a resource (P6) from the managed system are properly executed.

    Inter-Behavior Specification Properties

    Inter-behavior properties allow verification of properties about the interaction between multiple behaviors of a MAPE-K loop.

    P7: Analyze(X).Unsatisfied --> Plan(X).AddResource
    P8: Plan(X).ReleasePlanReady --> Execute(X).ExecuteRelease
    P9: Plan(X).AddPlanReady --> Execute(X).ExecuteAdd

    P7 describes a property to verify the correct collaboration between the Analyze and Plan behaviors. The property states that when Analyze detects an unsatisfactory state of the managed system, eventually the Plan behavior will starts planning to find a resource. P8 and P9 describe properties to verify the correct collaboration between Plan and Execute behaviors. In particular, P8 allows to verify that when Plan has generated a plan to release a resource, this plan is eventually executed by the Execute

Last update: November 2, 2013 - feedback