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. <dt.>
The primary goal of this dissertation is to obtain the capability to decide the correctness of graph-based specifications consisting of a graphical precondition, a graph program, and a graphical postcondition. It is shown how to construct weakest preconditions for graph programs and graph conditions. Moreover, a sound and complete satisfiability algorithm for graph conditions is investigated and a fragment of conditions is identified, for which the algorithm decides. On the other hand, a resolution-based calculus for proving graph conditions is presented and its soundness is proven. Implementations of the aforementioned deciders for conditions are compared with existing theorem provers and satisfiability solvers for first-order logic by verifying three case studies: a railroad control, an access control for computer systems, and, as an external example, a car platoon maneuver protocol. <engl.>
Seite 3 von 6
