Development of correct graph transformation systems

Primäres Ziel dieser Dissertation ist die Erlangung der Fähigkeit die Korrektheit von graphenbasierten Spezifikationen zu entscheiden, die aus einer grafischen Vorbedingung, einem Graphprogramm und einer grafischen Nachbedingung bestehen. Es wird gezeigt, wie schwächste Vorbedingungen für Graphprogramme und Graphbedingungen konstruiert werden. Ferner wird ein korrekter und vollständiger Erfüllbarkeitsalgorithmus für Graphbedingungen untersucht und ein Fragment von Graphbedingungen identifiziert, für das der Algorithmus entscheidet. Andererseits wird ein resolutionsbasierter Kalkül für das Beweisen von Graphbedingungen präsentiert und seine Korrektheit bewiesen. Implementierungen der zuvor genannten Komponenten werden mit bestehenden Werkzeugen für Logik erster Stufe anhand dreier Fallstudien verglichen: einem Eisenbahnkontrollsystem, einer Zugangskontrolle für Computersysteme und, als externe Fallstudie, einem Protokoll für Manöver von Autokolonnen.

Level thesis:degree_level

thesis.doctoral

Grantor dc:publisher

Universität Oldenburg

Year

2009

Author dc:creator

• Pennemann, Karl-Heinz

• Graph transformation system , correctness

Repository record source_url

http://oops.uni-oldenburg.de/884

OAI identifier oai:identifier

oai:oops.uni-oldenburg.de:884