TY - BOOK A1 - Flotterer, Boris A1 - Maximova, Maria A1 - Schneider, Sven A1 - Dyck, Johannes A1 - Zöllner, Christian A1 - Giese, Holger A1 - Hély, Christelle A1 - Gaucherel, Cédric T1 - Modeling and Formal Analysis of Meta-Ecosystems with Dynamic Structure using Graph Transformation T3 - Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam N2 - The dynamics of ecosystems is of crucial importance. Various model-based approaches exist to understand and analyze their internal effects. In this paper, we model the space structure dynamics and ecological dynamics of meta-ecosystems using the formal technique of Graph Transformation (short GT). We build GT models to describe how a meta-ecosystem (modeled as a graph) can evolve over time (modeled by GT rules) and to analyze these GT models with respect to qualitative properties such as the existence of structural stabilities. As a case study, we build three GT models describing the space structure dynamics and ecological dynamics of three different savanna meta-ecosystems. The first GT model considers a savanna meta-ecosystem that is limited in space to two ecosystem patches, whereas the other two GT models consider two savanna meta-ecosystems that are unlimited in the number of ecosystem patches and only differ in one GT rule describing how the space structure of the meta-ecosystem grows. In the first two GT models, the space structure dynamics and ecological dynamics of the meta-ecosystem shows two main structural stabilities: the first one based on grassland-savanna-woodland transitions and the second one based on grassland-desert transitions. The transition between these two structural stabilities is driven by high-intensity fires affecting the tree components. In the third GT model, the GT rule for savanna regeneration induces desertification and therefore a collapse of the meta-ecosystem. We believe that GT models provide a complementary avenue to that of existing approaches to rigorously study ecological phenomena. N2 - Die Dynamik von Ökosystemen ist von entscheidender Bedeutung. Es gibt verschiedene modellbasierte Ansätze, um ihre internen Effekte zu verstehen und zu analysieren. In diesem Beitrag modellieren wir die Raumstrukturdynamik und ökologische Dynamik von Metaökosystemen mit der formalen Technik der Graphtransformation (kurz GT). Wir bauen GT-Modelle, um zu beschreiben, wie sich ein Meta-Ökosystem (modelliert als Graph) im Laufe der Zeit entwickeln kann (modelliert durch GT-Regeln) und analysieren diese GT-Modelle hinsichtlich qualitativer Eigenschaften wie das Vorhandensein struktureller Stabilitäten. Als Fallstudie bauen wir drei GT-Modelle, die die Dynamik der Raumstruktur und die ökologische Dynamik von drei verschiedenen Savannen-Meta-Ökosystemen beschreiben. Das erste GT-Modell betrachtet ein Savannen-Meta-Ökosystem, das räumlich auf zwei Ökosystem-Abschnitte begrenzt ist, während die anderen beiden GT-Modelle zwei Savannen-Meta-Ökosysteme betrachten, die in der Anzahl von Ökosystem-Abschnitten uneingeschränkt sind und sich nur in einer GT-Regel unterscheiden, die beschreibt, wie die Raumstruktur des Meta-Ökosystems wächst. In den ersten beiden GT-Modellen zeigen die Raumstrukturdynamik und die ökologische Dynamik des Metaökosystems zwei Hauptstrukturstabilitäten: die erste basiert auf Grasland-Savannen-Wald-Übergängen und die zweite basiert auf Grasland-Wüsten-Übergängen. Der Übergang zwischen diesen beiden strukturellen Stabilitäten wird durch hochintensive Brände angetrieben, die die Baumkomponenten beeinträchtigen. Beim dritten GT-Modell führt die Savannenregeneration beschreibende GT-Regel zur Wüstenbildung und damit zum Kollaps des Meta-Ökosystems. Wir glauben, dass GT-Modelle eine gute Ergänzung zu bestehenden Ansätzen darstellen, um ökologische Phänomene rigoros zu untersuchen. T3 - Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam - 147 KW - dynamic systems KW - discrete-event model KW - qualitative model KW - savanna KW - trajectories KW - desertification KW - dynamische Systeme KW - diskretes Ereignismodell KW - qualitatives Modell KW - Savanne KW - Trajektorien KW - Wüstenbildung Y1 - 2022 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-547643 SN - 978-3-86956-533-0 SN - 1613-5652 SN - 2191-1665 IS - 147 PB - Universitätsverlag Potsdam CY - Potsdam ER - TY - JOUR A1 - Dyck, Johannes A1 - Giese, Holger A1 - Lambers, Leen T1 - Automatic verification of behavior preservation at the transformation level for relational model transformation JF - Software and systems modeling N2 - The correctness of model transformations is a crucial element for model-driven engineering of high-quality software. In particular, behavior preservation is an important correctness property avoiding the introduction of semantic errors during the model-driven engineering process. Behavior preservation verification techniques show some kind of behavioral equivalence or refinement between source and target model of the transformation. Automatic tool support is available for verifying behavior preservation at the instance level, i.e., for a given source and target model specified by the model transformation. However, until now there is no sound and automatic verification approach available at the transformation level, i.e., for all source and target models. In this article, we extend our results presented in earlier work (Giese and Lambers, in: Ehrig et al (eds) Graph transformations, Springer, Berlin, 2012) and outline a new transformation-level approach for the sound and automatic verification of behavior preservation captured by bisimulation resp.simulation for outplace model transformations specified by triple graph grammars and semantic definitions given by graph transformation rules. In particular, we first show how behavior preservation can be modeled in a symbolic manner at the transformation level and then describe that transformation-level verification of behavior preservation can be reduced to invariant checking of suitable conditions for graph transformations. We demonstrate that the resulting checking problem can be addressed by our own invariant checker for an example of a transformation between sequence charts and communicating automata. KW - Relational model transformation KW - Formal verification of behavior preservation KW - Behavioral equivalence and refinement KW - Bisimulation and simulation KW - Graph transformation KW - Triple graph grammars KW - Invariant checking Y1 - 2018 U6 - https://doi.org/10.1007/s10270-018-00706-9 SN - 1619-1366 SN - 1619-1374 VL - 18 IS - 5 SP - 2937 EP - 2972 PB - Springer CY - Heidelberg ER - 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 -