Mit Graphprogrammen können viele Arten diskreter Systeme formal modelliert werden. Es sind Graphersetzungssysteme mit Kontrollstrukturen (Sequenz, Auswahl und Iteration). In dieser Arbeit werden ein theoretisch begründeter Formalismus zum Spezifizieren von Eigenschaften von Graphprogrammen sowie ein Verfahren zum Nachweis der partiellen Korrektheit von Graphprogrammen eingeführt. Rekursiv geschachtelte Graphbedingungen (mu-Bedingungen) sind eine neue Spezifikationssprache, die nichtlokale Zustandseigenschaften ausdrücken kann und sich nachweislich von anderen Formalismen unterscheidet. Der Verifikationsansatz besteht aus: - einer Übertragung von Dijkstras Kalkül der schwächsten Vorbedingungen auf Graphprogramme und mu-Bedingungen - einem Beweiskalkül für mu-Bedingungen, dessen Kernstück ein Regelschema für induktive Widerlegung ist. Desweiteren werden innerhalb desselben Frameworks Korrektheit unter widrigen Umständen und strukturveränderliche Petrinetze betrachtet. <dt.>
With graph programs, one can formally model the behaviour of a wide range of discrete systems. These programs extend graph rewriting by control structures (sequence, choice and iteration). This thesis presents a theoretically founded formalism for specifying properties of graph programs and a proof-based approach to verifying the partial correctness of a graph program relative to a pre- and postcondition. A novel specification language, recursively nested conditions (mu-conditions) is introduced, which can express nonlocal state properties and which is shown to be distinct from other relevant formalisms. The verification approach consists of: - an adaptation of Dijkstra's weakest precondition calculus to graph programs and mu-conditions, - a proof calculus for mu-conditions, whose core part is a rule schema for inductive refutation. Additionally, a formulation of correctness under adversity and structure-changing Petri nets are elaborated within the same framework. <engl.>
Graphtransformationssysteme sind ein graphbasierter Ansatz zur visuellen Modellierung und ermöglichen einen intuitiven Blick auf ein System. Systemeigenschaften können durch geschachtelte Bedingungen (Habel, Pennemann 2009) dargestellt werden. Diese können keine nichtlokalen Eigenschaften wie Pfade, Verbundenheit oder Kreisfreiheit ausdrücken. Wir führen daher HR*-Bedingungen ein, die geschachtelte Bedingungen um Hyperkantenersetzung erweitern, und erörtern deren Ausdruckskraft. Eine Methode zur Prüfung der Korrektheit einer Spezifikation aus Programm, Vor- und Nachbedingung wird eingeführt, auf Basis grundlegender Transformationen der Bedingungen. HR*-Bedingungen werden ferner angewendet, um Instanzen von UML-Metamodellen mit OCL-Bedingungen zu erzeugen. Der Typgraph wird zu einer Grammatik umgewandelt. Die OCL-Bedingungen werden in HR*-Bedingungen umgewandelt und als Anwendungsbedingungen in die Graphgrammatik integriert, was die Erzeugung valider Instanzen des Modells garantiert. <dt.>
Graph transformation systems are an established visual modeling approach, using graphs to give an intuitive overview of a system. Structural system properties can be expressed by nested conditions (Habel, Pennemann 2009). However, nested conditions can not express non-local properties, like arbitrary-length paths, connectedness or circle-freeness. We propose HR* conditions, extending nested conditions with hyperedge replacement. The expressiveness of several variants HRs conditions is discussed. A method is presented to check the correctness of a specification consisting of a graph program with HR* pre- and postcondition, by utilizing basic transformations on the conditions. HR* conditions are used to generate instances of UML meta-models with OCL constraints. The type graph is transformed into a graph grammar. OCL constraints are transformed into HR* conditions, which are then integrated into the graph grammar as application conditions to ensure the generation of valid instances. <engl.>
