Development of correct graph transformation systems

Abstract

A major goal of this thesis is the ability to determine the correctness of graphical specifications consisting of a graph precondition, a graph program and graph postcondition. 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 precondition implies the weakest precondition. With the intention of tool support, we investigate the construction of weakest graph preconditions, consider fragments of graph conditions, for which the implication problem is decidable, and investigate an approximative solution of said problem in the general case. All research is done within the framework of adhesive high-level replacement categories. Therefore, the results will be applicable to different kinds of transformation systems and petri nets. © 2008 Springer-Verlag Berlin Heidelberg.