Achieving Adaptation for Adaptive Systems via Runtime Verification: A Model-Driven Approach

TL;DR

This paper presents a model-driven method for enabling self-adaptive systems to automatically meet non-functional requirements like reliability and performance through runtime verification and formal modeling.

Contribution

It introduces a novel approach that integrates goal models, behavior models, and Markov chains to support runtime adaptation decisions based on NFRs.

Findings

Successfully applied to a mobile information system

Effectively verifies NFR compliance at runtime

Enhances automatic adaptation in self-adaptive systems

Abstract

Self-adaptive systems (SASs) are capable of adjusting its behavior in response to meaningful changes in the operational con-text and itself. The adaptation needs to be performed automatically through self-managed reactions and decision-making processes at runtime. To support this kind of automatic behavior, SASs must be endowed by a rich runtime support that can detect requirements violations and reason about adaptation decisions. Requirements Engineering for SASs primarily aims to model adaptation logic and mechanisms. Requirements models will guide the design decisions and runtime behaviors of sys-tem-to-be. This paper proposes a model-driven approach for achieving adaptation against non-functional requirements (NFRs), i.e. reliability and performances. The approach begins with the models in RE stage and provides runtime support for self-adaptation. We capture adaptation mechanisms as graphical elements in the goal model. By assigning reliability and performance attributes to related system tasks, we derive the tagged sequential diagram for specifying the reliability and performances of system behaviors. To formalize system behavior, we transform the requirements model to the corresponding behavior model, expressed by Label Transition Systems (LTS). To analyze the reliability requirements and performance requirements, we merged the sequential diagram and LTS to a variable Discrete-Time Markov Chains (DTMC) and a variable Continuous-Time Markov Chains (CTMC) respectively. Adaptation candidates are characterized by the variable states. The optimal decision is derived by verifying the concerned NFRs and reducing the decision space. Our approach is implemented through the demonstration of a mobile information system.