TY - THES A1 - Dyck, Johannes T1 - Verification of graph transformation systems with k-inductive invariants T1 - Verifikation von Graphtransformationssystemen mit k-induktiven Invarianten N2 - With rising complexity of today's software and hardware systems and the hypothesized increase in autonomous, intelligent, and self-* systems, developing correct systems remains an important challenge. Testing, although an important part of the development and maintainance process, cannot usually establish the definite correctness of a software or hardware system - especially when systems have arbitrarily large or infinite state spaces or an infinite number of initial states. This is where formal verification comes in: given a representation of the system in question in a formal framework, verification approaches and tools can be used to establish the system's adherence to its similarly formalized specification, and to complement testing. One such formal framework is the field of graphs and graph transformation systems. Both are powerful formalisms with well-established foundations and ongoing research that can be used to describe complex hardware or software systems with varying degrees of abstraction. Since their inception in the 1970s, graph transformation systems have continuously evolved; related research spans extensions of expressive power, graph algorithms, and their implementation, application scenarios, or verification approaches, to name just a few topics. This thesis focuses on a verification approach for graph transformation systems called k-inductive invariant checking, which is an extension of previous work on 1-inductive invariant checking. Instead of exhaustively computing a system's state space, which is a common approach in model checking, 1-inductive invariant checking symbolically analyzes graph transformation rules - i.e. system behavior - in order to draw conclusions with respect to the validity of graph constraints in the system's state space. The approach is based on an inductive argument: if a system's initial state satisfies a graph constraint and if all rules preserve that constraint's validity, we can conclude the constraint's validity in the system's entire state space - without having to compute it. However, inductive invariant checking also comes with a specific drawback: the locality of graph transformation rules leads to a lack of context information during the symbolic analysis of potential rule applications. This thesis argues that this lack of context can be partly addressed by using k-induction instead of 1-induction. A k-inductive invariant is a graph constraint whose validity in a path of k-1 rule applications implies its validity after any subsequent rule application - as opposed to a 1-inductive invariant where only one rule application is taken into account. Considering a path of transformations then accumulates more context of the graph rules' applications. As such, this thesis extends existing research and implementation on 1-inductive invariant checking for graph transformation systems to k-induction. In addition, it proposes a technique to perform the base case of the inductive argument in a symbolic fashion, which allows verification of systems with an infinite set of initial states. Both k-inductive invariant checking and its base case are described in formal terms. Based on that, this thesis formulates theorems and constructions to apply this general verification approach for typed graph transformation systems and nested graph constraints - and to formally prove the approach's correctness. Since unrestricted graph constraints may lead to non-termination or impracticably high execution times given a hypothetical implementation, this thesis also presents a restricted verification approach, which limits the form of graph transformation systems and graph constraints. It is formalized, proven correct, and its procedures terminate by construction. This restricted approach has been implemented in an automated tool and has been evaluated with respect to its applicability to test cases, its performance, and its degree of completeness. N2 - Durch die Komplexität heutiger Software- und Hardwaresysteme und den vermuteten Anstieg der Zahl autonomer und intelligenter Systeme bleibt die Entwicklung korrekter Systeme eine wichtige Herausforderung. Obwohl Testen ein wichtiger Teil des Entwicklungszyklusses ist und bleibt, reichen Tests üblicherweise nicht aus, um die Korrektkeit eines Systems sicherzustellen - insbsondere wenn Systeme beliebig große oder unendliche Zustandsräume oder unendlich viele mögliche initiale Zustände aufweisen. Formale Verifikation nimmt sich dieses Problems an: Nach Darstellung des Systems in einem formalen Modell können Verifikationsansätze und Werkzeuge angewendet werden, um zu analysieren, ob das System seine Spezifikation erfüllt. Ein verbreiteter Formalismus für derartige Modelle sind Graphen und Graphtransformationssysteme. Diese Konzepte basieren auf etablierten mathematischen Grundlagen und sind ausdrucksstark genug, um komplexe Software- oder Hardwaresysteme auf verschiedenen Abstraktionsstufen zu beschreiben. Seit ihrer Einführung in den 70er-Jahren wurden Graphtransformationssysteme stetig weiterentwickelt; entsprechende Forschung thematisiert beispielsweise Ausdrucksstärke, Graphalgorithmen, Anwendungsbeispiele oder Verifikationsansätze. Diese Arbeit beschäftigt sich mit der Verifikation k-induktiver Invarianten für Graphtransformationssysteme - einem Ansatz, der eine existierende Technik zur Verifikation 1-induktiver Invarianten erweitert. Anstatt den Zustandsraum eines Systems zu berechnen, überprüft Verifikation mit 1-Induktion Verhalten (Graphtransformationsregeln) symbolisch, um Schlussfolgerungen zur Gültigkeit von Graphbedingungen zu ziehen. Die Idee basiert auf dem Prinzip eines Induktionsbeweises: Falls der initiale Zustand eines Systems eine Bedingung erfüllt und falls alle Regeln die Erfüllung der Bedingung bewahren, kann auf die Gültigkeit der Bedingung im gesamten Zustandsraum geschlossen werden, ohne diesen tatsächlich zu berechnen. Allerdings bringt dieser Ansatz auch spezifische Nachteile mit sich: Die lokale Natur der Anwendung von Graphregeln führt zu einem Mangel an Kontext während der symbolischen Analyse möglicher Regelanwendungen. Diese Arbeit führt aus, dass dieser Mangel an Kontext teilweise behoben werden kann, indem k-Induktion statt 1-Induktion verwendet wird. Eine k-induktive Invariante ist eine Graphbedingung, deren Gültigkeit in einem Pfad von k-1 Regelanwendungen die Gültigkeit nach jeder etwaigen weiteren Regelanwendung zur Folge hat. Durch die Berücksichtigung solcher Pfade von Transformationen steht mehr Kontext während der Analyse zur Verfügung als bei der Analyse nur einer Regelanwendung bei 1-Induktion. Daher erweitert diese Arbeit bestehende Forschungsergebnisse und eine Implementierung zur Verifikation 1-induktiver Invarianten um k-Induktion. Zusätzlich wird eine Technik vorgestellt, die auch die Analyse der Induktionsbasis symbolisch ausführt. Dies erlaubt die Verifikation von Systemen mit einer unendlichen Zahl an möglichen initialen Zuständen. Sowohl k-induktive Invarianten als auch deren Induktionsbasis werden - für Graphtransformationssysteme - formal beschrieben. Basierend darauf stellt diese Arbeit Theoreme und Kontruktionen vor, die diesen Verifikationsansatz mathemathisch umsetzen und seine Korrektheit beweisen. Da jedoch uneingeschränkte Graphbedingungen in einer möglichen Implementierung zu Nichtterminierung oder langen Ausführungszeiten führen, stellt diese Arbeit auch einen eingeschränkten Verifikationsansatz vor, der die Form der zugelassenen Graphtransformationssysteme und Graphbedingungen in Spezifikationen einschränkt. Auch dieser Ansatz wird formalisiert, bewiesen - und das Verfahren terminiert per Konstruktion. Der Ansatz wurde in Form eines automatisch ausführbaren Verifikationswerkzeugs implementiert und wurde in Bezug auf seine Anwendbarkeit, Performanz und des Grades der Vollständigkeit evaluiert. KW - formal verification KW - graph transformations KW - inductive invariant checking KW - k-induction KW - graph constraints KW - application conditions KW - k-inductive invariant KW - graph transformation systems KW - formale Verifikation KW - Graphtransformationen KW - Verifikation induktiver Invarianten KW - k-Induktion KW - Graphbedingungen KW - Anwendungsbedingungen KW - k-induktive Invariante KW - Graphtransformationssysteme Y1 - 2020 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-442742 ER - TY - THES A1 - Vogel, Thomas T1 - Model-driven engineering of self-adaptive software T1 - Modellgetriebene Entwicklung von Selbst-Adaptiver Software N2 - The development of self-adaptive software requires the engineering of an adaptation engine that controls the underlying adaptable software by a feedback loop. State-of-the-art approaches prescribe the feedback loop in terms of numbers, how the activities (e.g., monitor, analyze, plan, and execute (MAPE)) and the knowledge are structured to a feedback loop, and the type of knowledge. Moreover, the feedback loop is usually hidden in the implementation or framework and therefore not visible in the architectural design. Additionally, an adaptation engine often employs runtime models that either represent the adaptable software or capture strategic knowledge such as reconfiguration strategies. State-of-the-art approaches do not systematically address the interplay of such runtime models, which would otherwise allow developers to freely design the entire feedback loop. This thesis presents ExecUtable RuntimE MegAmodels (EUREMA), an integrated model-driven engineering (MDE) solution that rigorously uses models for engineering feedback loops. EUREMA provides a domain-specific modeling language to specify and an interpreter to execute feedback loops. The language allows developers to freely design a feedback loop concerning the activities and runtime models (knowledge) as well as the number of feedback loops. It further supports structuring the feedback loops in the adaptation engine that follows a layered architectural style. Thus, EUREMA makes the feedback loops explicit in the design and enables developers to reason about design decisions. To address the interplay of runtime models, we propose the concept of a runtime megamodel, which is a runtime model that contains other runtime models as well as activities (e.g., MAPE) working on the contained models. This concept is the underlying principle of EUREMA. The resulting EUREMA (mega)models are kept alive at runtime and they are directly executed by the EUREMA interpreter to run the feedback loops. Interpretation provides the flexibility to dynamically adapt a feedback loop. In this context, EUREMA supports engineering self-adaptive software in which feedback loops run independently or in a coordinated fashion within the same layer as well as on top of each other in different layers of the adaptation engine. Moreover, we consider preliminary means to evolve self-adaptive software by providing a maintenance interface to the adaptation engine. This thesis discusses in detail EUREMA by applying it to different scenarios such as single, multiple, and stacked feedback loops for self-repairing and self-optimizing the mRUBiS application. Moreover, it investigates the design and expressiveness of EUREMA, reports on experiments with a running system (mRUBiS) and with alternative solutions, and assesses EUREMA with respect to quality attributes such as performance and scalability. The conducted evaluation provides evidence that EUREMA as an integrated and open MDE approach for engineering self-adaptive software seamlessly integrates the development and runtime environments using the same formalism to specify and execute feedback loops, supports the dynamic adaptation of feedback loops in layered architectures, and achieves an efficient execution of feedback loops by leveraging incrementality. N2 - Die Entwicklung von selbst-adaptiven Softwaresystemen erfordert die Konstruktion einer geschlossenen Feedback Loop, die das System zur Laufzeit beobachtet und falls nötig anpasst. Aktuelle Konstruktionsverfahren schreiben eine bestimmte Feedback Loop im Hinblick auf Anzahl und Struktur vor. Die Struktur umfasst die vorhandenen Aktivitäten der Feedback Loop (z. B. Beobachtung, Analyse, Planung und Ausführung einer Adaption) und die Art des hierzu verwendeten Systemwissens. Dieses System- und zusätzlich das strategische Wissen (z. B. Adaptionsregeln) werden in der Regel in Laufzeitmodellen erfasst und in die Feedback Loop integriert. Aktuelle Verfahren berücksichtigen jedoch nicht systematisch die Laufzeitmodelle und deren Zusammenspiel, so dass Entwickler die Feedback Loop nicht frei entwerfen und gestalten können. Folglich wird die Feedback Loop während des Entwurfs der Softwarearchitektur häufig nicht explizit berücksichtigt. Diese Dissertation stellt mit EUREMA ein neues Konstruktionsverfahren für Feedback Loops vor. Basierend auf Prinzipien der modellgetriebenen Entwicklung (MDE) setzt EUREMA auf die konsequente Nutzung von Modellen für die Konstruktion, Ausführung und Adaption von selbst-adaptiven Softwaresystemen. Hierzu wird eine domänenspezifische Modellierungssprache (DSL) vorgestellt, mit der Entwickler die Feedback Loop frei entwerfen und gestalten können, d. h. ohne Einschränkung bezüglich der Aktivitäten, Laufzeitmodelle und Anzahl der Feedback Loops. Zusätzlich bietet die DSL eine Architektursicht auf das System, die die Feedback Loops berücksichtigt. Daher stellt die DSL Konstrukte zur Verfügung, mit denen Entwickler während des Entwurfs der Architektur die Feedback Loops explizit definieren und berücksichtigen können. Um das Zusammenspiel der Laufzeitmodelle zu erfassen, wird das Konzept eines sogenannten Laufzeitmegamodells vorgeschlagen, das alle Aktivitäten und Laufzeitmodelle einer Feedback Loop erfasst. Dieses Konzept dient als Grundlage der vorgestellten DSL. Die bei der Konstruktion und mit der DSL erzeugten (Mega-)Modelle werden zur Laufzeit bewahrt und von einem Interpreter ausgeführt, um das spezifizierte Adaptionsverhalten zu realisieren. Der Interpreteransatz bietet die notwendige Flexibilität, um das Adaptionsverhalten zur Laufzeit anzupassen. Dies ermöglicht über die Entwicklung von Systemen mit mehreren Feedback Loops auf einer Ebene hinaus das Schichten von Feedback Loops im Sinne einer adaptiven Regelung. Zusätzlich bietet EUREMA eine Schnittstelle für Wartungsprozesse an, um das Adaptionsverhalten im laufendem System anzupassen. Die Dissertation diskutiert den EUREMA-Ansatz und wendet diesen auf verschiedene Problemstellungen an, u. a. auf einzelne, mehrere und koordinierte als auch geschichtete Feedback Loops. Als Anwendungsbeispiel dient die Selbstheilung und Selbstoptimierung des Online-Marktplatzes mRUBiS. Für die Evaluierung von EUREMA werden Experimente mit dem laufenden mRUBiS und mit alternativen Lösungen durchgeführt, das Design und die Ausdrucksmächtigkeit der DSL untersucht und Qualitätsmerkmale wie Performanz und Skalierbarkeit betrachtet. Die Ergebnisse der Evaluierung legen nahe, dass EUREMA als integrierter und offener Ansatz für die Entwicklung selbst-adaptiver Softwaresysteme folgende Beiträge zum Stand der Technik leistet: eine nahtlose Integration der Entwicklungs- und Laufzeitumgebung durch die konsequente Verwendung von Modellen, die dynamische Anpassung des Adaptionsverhaltens in einer Schichtenarchitektur und eine effiziente Ausführung von Feedback Loops durch inkrementelle Verarbeitungsschritte. KW - model-driven engineering KW - self-adaptive software KW - domain-specific modeling KW - runtime models KW - software evolution KW - modellgetriebene Entwicklung KW - Selbst-Adaptive Software KW - Domänenspezifische Modellierung KW - Laufzeitmodelle KW - Software-Evolution Y1 - 2018 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-409755 ER -