Development of correct graph transformation systems [Elektronische Ressource] / vorgelegt von Karl-Heinz Pennemann

Karl-Heinz Pennemann

Sujets

• Informatik

Informations

• Publié par: carl_von_ossietzky_universitat_oldenburg
• Publié le: 01 janvier 2009
• Nombre de lectures: 6
• Langue: English
• Poids de l'ouvrage: 2 Mo

Extrait

Fakultät II – Informatik, Wirtschafts- und Rechtswissenschaften
Department für Informatik
Development of Correct
Graph Transformation Systems
Dissertation zur Erlangung des Grades eines
Doktors der Naturwissenschaften
vorgelegt von
Dipl.-Inform. Karl-Heinz Pennemann
Oldenburg, 18. Mai 2009ii Development of Correct Graph Transformation Systems
Prüfungskommision
Vorsitzender: Prof. Dr. Martin-Fränzle
Gutachterin: Prof. Dr. Annegret Habel
Gutachter: Prof. Dr. Ernst-Rüdiger Olderog
Gutachter: Prof. Dr. Arend Rensink
Mitglied: Dr. Sybille Fröschle
Datum der Disputation: 11. September 2009Development of Correct Graph Transformation Systems iii
Abstract
Graph transformation has many application areas in computer science, such
as software engineering or the design of concurrent and distributed systems.
Being a visual modeling technique, graph transformation has the potential
to play a decisive role in the development of increasingly larger and complex
systems. However, the use of visual modeling techniques alone does not
guarantee the correctness of a design. In context of rising standards for
trustworthy systems, there is a growing need for the verification of graph
transformation systems and programs. The research of appropriate methods
for this purpose is the topic of this thesis.
The primary goal is to obtain the capability to decide graphical program
specifications. These specifications consists of a graphical precondition, a
graphprogram, anda graphicalpostcondition. Asusual, such a specification
is said to be correct, if all those system states satisfy the postcondition that
are reachable by applying the program on a start state satisfying the pre-
condition. In the considered programs, the selection, deletion, addition and
deselection of a graph’s nodes and edges are the elementary constructs that
can be composed to more complex programs by non-deterministic choice, se-
quential composition and iteration. The resulting programming language is
computationally complete and is able to model transactions that deal with
an unbounded number of nodes and edges. As language for the specification
of state properties, graph conditions are investigated and used. We show
that graph conditions provide an intuitive formalism for first-order struc-
tural properties and are suited to infer knowledge about the behavior of
graph transformation systems and programs.
According to Dijkstra, the correctness of program specifications can be
shown by constructing a weakest precondition of the program relative to the
postcondition and checking whether the specified precondition implies the
weakest precondition. Hence the correctness problem of program specifica-
tions is reduced to an implication problem of conditions. In this thesis, it is
shown how toconstruct weakest preconditions forgraphprogramsandgraph
conditions. Following a dual approach, a sound and complete satisfiabilityiv Development of Correct Graph Transformation Systems
algorithmforgraphconditions isinvestigated andafragmentof conditions is
identified, for which the algorithm decides. On the other hand, a resolution-
based calculus for graph conditions is presented and its soundness is proven.
Implementations of the aforementioned deciders for conditions are compared
with existing theorem provers andsatisfiability solvers forfirst-order logicby
verifyingthreecasestudies: arailroadcontrol,anaccesscontrolforcomputer
systems, and, as an external example, a car platoon maneuver protocol.
The research is done within the framework of the so-called weak adhesive
high-level replacement categories. Therefore, the results will be applicable
to different kinds of graph replacement systems and Petri nets, providing
theoretical fundamentalsandgeneralconcepts forthedevelopment ofcorrect
transformation-based systems and programs.Development of Correct Graph Transformation Systems v
Zusammenfassung
Graphtransformation hat viele Anwendungsgebiete in der Informatik, zum
BeispielimSoftwareentwurf oderinderModellierungvonnebenläufigenoder
verteiltenSystemen.AlsvisuelleModellierungstechnikhatGraphtransforma-
tion das Potenzial, eine entscheidende Rolle in der Entwicklung von immer
größer und komplexer werdenden Systemen einzunehmen. Allerdings garan-
tiert die Benutzung einer visuellen Modellierungstechnik noch nicht die Kor-
rektheit eines Modells. Im Hinblick auf steigende Standards für vertrauens-
würdige Systeme ergibt sich ein wachsendes Interesse an der Verifikation von
Graphtransformationssystemen und -programmen. Die Entwicklung entspre-
chender Methoden zu diesem Zweck ist das Thema dieser Dissertation.
PrimäresZielistdieErlangungderFähigkeit,grafischeProgrammspezifi-
kationen zu entscheiden. Diese Spezifikationen bestehen aus einer grafischen
Vorbedingung, einem Graphprogramm und einer grafischen Nachbedingung.
Man nennt eine solche Spezifikation korrekt, wenn diejenigen Systemzustän-
de der Nachbedingung genügen, die durch Ausführung des Graphprogramms
von einem die Vorbedingung erfüllenden Startzustand aus erreichbar sind. In
denbetrachtetenProgrammensinddasSelektieren,Löschen,Hinzufügenund
Deselektieren von Knoten und Kanten eines Graphen die elementaren Kon-
strukte, die durch nichtdeterministische Auswahl, sequentielle Komposition
und Iteration zu komplexeren Programmen verknüpfbar sind. Die entstehen-
de Programmiersprache ist Turing-vollständig und erlaubt beispielsweise die
Modellierung von Transaktionen, die eine unbeschränkte Anzahl von Knoten
und Kanten betreffen. Als Beschreibungssprache für Zustandseigenschaften
werden Graphbedingungen untersucht und benutzt. Es wird gezeigt, dass
Graphbedingungen einen intuitiven Formalismus für Struktureigenschaften
erster Stufe bereit stellen und darüber hinaus geeignet sind, Informationen
über das Verhalten von Systemen und Programmen abzuleiten.
DieKorrektheitvonProgrammspezifikationenkann,nachDijkstra,unter-
sucht werden durch Konstruktion einer schwächsten Vorbedingung aus dem
Programm relativ zur Nachbedingung und durch Entscheiden, ob die spe-
zifizierte Vorbedingung die schwächste Vorbedingung impliziert. In diesemvi Development of Correct Graph Transformation Systems
Sinne wird das Problem der Korrektheit von Programmspezifikationen auf
das Implikationsproblem von Bedingungen reduziert. In dieser Arbeit wird
gezeigt,wie schwächste VorbedingungenfürGraphprogrammeundGraphbe-
dingungen konstruiert werden. Einem dualen Ansatz folgend, wird einerseits
ein korrekter und vollständiger Erfüllbarkeitsalgorithmus für Graphbedin-
gungenuntersucht undeinFragmentvonGraphbedingungenidentifiziert,für
das der Algorithmus entscheidet. Andererseits wird ein resolutionsbasierter
Kalkül für das Beweisen von Graphbedingungen präsentiert und seine Kor-
rektheit bewiesen. Implementierungen der zuvor genannten Komponenten
werden mit bestehenden Werkzeugen für Logik erster Stufe anhand dreier
Fallstudien verglichen: einem Eisenbahnkontrollsystem, einer Zugangskon-
trolle für Computersysteme und, als externe Fallstudie, einem Protokoll für
Manöver von Autokolonnen.
DieUntersuchungenwerdeninnerhalbdesRahmenwerksdersogenannten
schwach adhesiven high-level Ersetzungskategorien durchgeführt. Die Ergeb-
nisse sind damit auf verschiedene Arten von Graphersetzungssystemen und
Petri-Netzen anwendbar und stellen ein generelles Konzept zur Entwicklung
von korrekten transformationsbasierten Systemen und Programmen dar.Development of Correct Graph Transformation Systems vii
Danksagung
DieseArbeitwurdedurchdieDeutscheForschungsgemeinschaft(GRK1076/1
GraduiertenkollegVertrauenswürdigeSoftwaresysteme) unterstützt.Ichdan-
ke den Leitern des Graduiertenkollegs für das in mich gesetzte Vertrauen.
Weiter danke ich allen, die mich während meiner Promotion fachlich oder
persönlich unterstützt und motiviert haben.
Ganz herzlich danke ich meiner Betreuerin Frau Prof. Annegret Habel,
den Gutachtern Herrn Prof. Ernst-Rüdiger Olderog und Herrn Prof. Arend
Rensink,denMitgliederndesPrüfungsausschusses HerrnProf.MartinFränz-
le und Frau Dr. Sibylle Fröschle, den Mitgliedern der Arbeitsgruppe Formale
Sprachen, ChristianZuckschwerdt, StefanMollundKarlAzab,unddenMit-
gliedern des Graduiertenkollegs. Mein ganz besonderer Dank gilt Birgitt und
unseren Familien.
Diese Arbeit widme ich Birgitt und unserem Kind.
“So little time,
so much to do.”
Winston Churchillviii Development of Correct Graph Transformation SystemsDevelopment of Correct Graph Transformation Systems ix
Contents
1 Introduction 1
2 Preliminaries 7
2.1 The category of graphs . . . . . . . . . . . . . . . . . . . . . . 7
2.2 Weak adhesive HLR categories . . . . . . . . . . . . . . . . . . 15
3 Conditions 19
3.1 Nested conditions . . . . . . . . . . . . . . . . . . . . . . . . . 19
3.2 Comparison ofM- andA-satisfiability . . . . . . . . . . . . . 23
3.3 Comparison of graph conditions and graph formulas . . . . . . 31
3.4 Summary and discussion . . . . . . . . . . . . . . . . . . . . . 42
4 Programs and transformation systems 43
4.1 Programs with interface . . . . . . . . . . . . . . . . . . . . . 43
4.2 Elimin