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.

Selbst-adaptive Systeme gewinnen immer mehr an Bedeutung, da sie sowohl in der Industrie als auch im alltäglichen Leben immer häufiger zum Einsatz kommen. Im Gegensatz zu nicht-adaptiven Systemen ist ein selbst-adaptives System in der Lage auf seine Umgebung zu reagieren. Hierzu beobachtet das System seine Umgebung kontinuierlich und passt sich entsprechend an, um ein zuvor festgelegtes Ziel zu erreichen. Abstraktionsgrad und Komplexität solcher Anpassungen können je nach Anwendungsdomäne variieren. So passt sich ein Smartphone an seine Umgebung an, indem es von LTE zu WLAN wechselt, wenn ein bereits bekanntes WLAN in Reichweite kommt. Oder ein autonom fahrendes Auto verringert seine Geschwindigkeit, wenn es sich einer Unfallstelle nähert. Die Umgebung des Systems, der sogenannte Kontext, agiert selbstständig und stellt fortwährend Anforderungen an das System, die das System nur erfüllen kann, indem es seine Konfiguration entsprechend anpasst. In vielen Anwendungsdomänen von selbst-adaptiven Systemen können solche Anforderungen sowohl funktional als auch nicht-funktional sein.

Diese Arbeit widmet sich explizit den nicht-funktionalen Eigenschaften solcher Anforderungen. Insbesondere stehen dabei Echtzeitanforderungen im Fokus, die den Wechsel zwischen verschiedenen Konfigurationen betreffen. Folglich beschäftigen wir uns mit selbst-adaptiven Echtzeitsystemen und nehmen deshalb an, dass Rekonfigurationen inhärent eine gewisse Zeitspanne benötigen. Zusätzlich bleibt die Herausforderung von selbst-adaptiven Systemen, dass der Kontext fortwährend Anforderungen stellt, bestehen. Um diese Anforderungen des Kontexts zu erfüllen, muss das System Rekonfigurationsentscheidungen treffen (entweder reaktiv oder sogar proaktiv). Allerdings ist das Verhalten des Kontexts oft nicht exakt vorhersehbar, da Wissen über das Verhalten des Kontexts meistens mit Unsicherheiten behaftet ist. Infolgedessen ist das Treffen von Rekonfigurationsentscheidungen für selbst-adaptive Echtzeitsysteme eine herausfordernde Aufgabe.

Der wissenschaftliche Beitrag dieser Arbeit, um diese Aufgabe zu lösen, ist zweiteilig aufgebaut. Als Erstes stellen wir einen Formalismus zur Spezifikation von validen (Re-)konfigurationen und ihren Eigenschaften vor, der auch nicht-funktionale Eigenschaften von Rekonfigurationen berücksichtigt. Als Zweites übersetzen wir diese Spezifikation in ein Rekonfigurationsmodell basierend auf dem spieltheoretischen Formalismus der Stochastic Priced Timed Games, um Rekonfigurationsentscheidungen zu treffen. Durch Anwendung von Model Checking synthetisieren wir aus dem Rekonfigurationsmodell eine sogenannte Strategie für das Spiel zwischen dem System und seinem Kontext. In diesem Spiel werden sicherheitskritische Anforderungen des Kontexts als Gewinnbedingung kodiert. Folglich versucht der Kontext-Spieler den System-Spieler zu einer Verletzung von sicherheitskritischen Anforderungen zu zwingen. Die synthetisierte Strategie garantiert dem System-Spieler jedoch den Kontext-Spieler immer zu besiegen. Damit kann keine Sequenz von Spielzügen des Kontexts zu einer Verletzung der sicherheitskritischen Anforderungen führen. Auf technischer Ebene wird die Strategiesynthese mit dem Model Checker Uppaal Stratego umgesetzt, der zusätzlich auch statistisches Model Checking unterstützt. Mithilfe von statistischem Model Checking sind wir in der Lage, die synthetisierten Strategien mit Hinblick auf nicht-funktionale Eigenschaften zu optimieren (z.B., Rekonfigurationskosten wie den Energieverbrauch von Rekonfigurationen). In der Evaluation zeigen wir die Anwendbarkeit des vorgestellten Ansatzes, indem wir für eine Menge von unterschiedlich großen Fallstudien Strategien synthetisieren. Hierbei lässt sich ein einstellbarer Trade-Off zwischen Effektivität und Effizienz beobachten.