Johannes Dyck

• 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 theWith 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.…
• 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 denDurch 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.…