Scen@rist: an approach for verifying self-adaptive systems using runtime scenarios

Scen@rist is an approach that uses scenarios as runtime entities for verifying self-adaptive systems. This approach consists of monitoring a running self-adaptive system, annotating its scenario-based behaviour specification with the probability of transitions between scenarios, and then verifying whether a set of reachability properties hold. This is performed by translating the scenario-based models and properties in their probabilistic state-based counterparts and applying a model checking technique.

Figure 1 illustrates an overview of the proposed approach, which consists of five main steps: model and property transformation, monitoring, model update process, verification, and notification. The approach also makes two assumptions: (i) the software engineer has modelled the system behaviour using scenarios specified as MSCs and has specified the desired properties in terms of scenarios, and (ii) the self-adaptive system implementation is in accordance with the modelled scenarios.

Fig. 1 - The Scen@rist overview

In Step 1, a back-end LTS specification is synthesised from the front-end MSC specification. Step 2 consists of monitoring the running self-adaptation system and extracting relevant information from it that will be used to keep both front-end and back-end specifications updated at runtime. In Step 3, during the model update process, both HMSC and LTS are annotated with scenario transition probabilities, which accounts for the relative frequency with which the execution control transfers directly from one scenario to another. In Step 4, the resulting PLTS can be used to perform runtime verification in order to find possible violations of the properties specified by the user using a model checker. If any violation is detected, then a notification service is invoked (Step 5), thus connecting the analysis with the adaptation planning phase.

Tele Assistance System (TAS)

Tele Assistance System is a service-based system that provides remote health-monitoring to patients with chronic diseases. In the original concept, TAS uses a combination of sensors embedded in a wearable device to take periodical measurements of the patient’s vital parameters (scenario VitalParamMonitor) and analyses them through medical services (scenario MedicalAnalysis). The analysis result may lead to the invocation of an alarm service (scenario Alarm) to call an ambulance, or the invocation of a pharmacy service to change drug type (scenario ChangeDrug) or dose (scenario ChangeDose). The same alarm service can be invoked directly by the patient by using a panic button (scenario PanicButton). The HMSC illustrated in Figure 2, and its constituent bMSCs, three of which are shown in Figure 3, have been created using the LoTuS tool and represent the system behaviour with its services.

Fig. 2 - The High-level Message Sequence Chart specification for the Tele Assistance System

Fig. 3 - Three bMSC scenarios for the Tele Assistance System

References

You can find more information here.