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

Traditional runtime quantitative verification approaches for self-adaptive systems usually rely on the use of state-transition models to describe the system behaviour and check property violation at runtime. More recently, some approaches have advocated the use of scenarios as a strategy for representing both the normal and adaptive system behaviour. However, the use of scenarios as a runtime entity that drives the system adaptation is still a challenge since many research issues regarding the use of scenarios to support analysis for enabling self-adjustment at runtime in software systems remain open. The aim of this paper is twofold. Firstly, we investigate the use of scenario-based approaches in self-adaptive systems via a systematic mapping study. Secondly, we introduce Scen@rist, an approach that uses scenarios as runtime entities for verifying self-adaptive systems. The 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. The applicability of the proposed tool has been demonstrated by two self-adaptive service-based systems taken from the literature.