Computing Reconfiguration Strategies for Self-Adaptive Real-Time Systems with Stochastic Priced Timed Games

Self-adaptive systems have gained momentum due to their rapidly growing use in industry and our everyday lives. In contrast to non-adaptive systems, a self-adaptive system is able to react to its environment by continuously observing its environment and performing corresponding adaptations to reach a specific goal. Adaptations depend on the application scenario, can be of various forms, and vary in their level of abstraction and level of complexity. For instance, a mobile phone adapts itself by switching from LTE to Wi-Fi automatically when a known network becomes available, or an autonomous car slows down due to a traffic accident ahead. The environment of the system (i.e., the so-called context) acts independent of the system and imposes requirements which the system can only satisfy by adapting its configuration accordingly. In many application areas of self-adaptive systems, these requirements can be both functional and non-functional. In this thesis, we focus on non-functional requirements w.r.t. these adaptations, with a special focus on real-time requirements w.r.t. changing configurations. Thus, we assume reconfigurations to inherently take a certain amount of time in the domain of self-adaptive real-time systems. Furthermore, a characteristic property of self-adaptive systems is the fact that they are surrounded by a contextual environment which perpetually imposes contextual requirements (e.g., for the configuration of the system). To satisfy these requirements, the system has to make reconfiguration decisions in a reactive or even proactive fashion. However, the future actions of the context (i.e., the environment) cannot be predicted exactly in advance as they are afflicted with many sources of uncertainties. To summarize, reasoning on reconfiguration decisions for self-adaptive real-time systems is a challenging task. The contribution of this thesis for solving this task is twofold. First, we present a specification formalism for defining the set of valid (re)configurations, as well as non-functional properties of these reconfigurations. Second, we translate the specification into a sound reconfiguration model based on the game-theoretic formalism of stochastic priced timed games for computing reconfiguration decisions. Using model checking, we synthesize a so-called strategy for a game between a system and its context where we encode safety-critical (contextual) requirements as winning condition (i.e., the goal of the context player is to force the system into a violation of safety-critical requirements). The synthesized strategy guarantees the system player to win the game against the context player. Thus, no sequence of context actions can lead to a violation of safety-critical requirements. The synthesis of the strategy is performed by the model checker Uppaal Stratego which also supports statistical model-checking. Based on statistical model checking, we optimize strategies even further w.r.t. non-functional properties besides real-time (e.g., reconfiguration costs as energy consumption). In the evaluation, we demonstrate the feasibility of the presented approach by applying the strategy synthesis to a set of differently sized case studies, while observing adjustable trade-offs between effectiveness and efficiency.