Static Verification Techniques for Attributed Graph Transformations

Graph transformation with its formal foundations and its broad range of theoretical results, on the one hand, and competitive tool support, on the other hand, constitutes an effective framework for model-driven software development. Within the last decade, the theory of algebraic graph transformations has been developed towards a comprehensive formal framework including several sophisticated results on modeling, analysing, and verifying graph transformation systems. Prominent theoretical results are the static verification of consistency constraints as well as static conflict detection and conflict resolution techniques. Consistency constraints provide means to declaratively define global assertions that must remain true. Conflict detection and resolution techniques provide means to statically discover potential unintended interactions of graph transformations. Based on the framework for algebraic graph transformations several model transformation tools were developed over the last years. However, in order to become suitable for the practical needs in every-day software engineering, these tool oriented graph transformation approaches integrate language concepts that go beyond the simple manipulation of plain graphs. An important concept is the treatment of data values such as integers, booleans, and strings. The integration of primitive data attributes within the graph structure is indispensable to model almost all realistic systems, since they combine the structural aspects of a system with data aspects such as computations of values. While in the last years, many advanced language concepts were adapted from the tool oriented approaches and integrated within the theory of algebraic graph transformations, there is currently no theoretical approach that appropriately reflects the de-facto data attribute handling approach of practical implementations. Thus, the main body of theoretical results does not immediately apply to those implemented approaches. As a result, current tool support for analysis and verification techniques of attributed graph transformation systems is rather limited. This thesis attempts to close this gap. To this end, a framework for attributed graph transformation systems is proposed. In contrast to existing approaches, the proposed framework reflects more closely the attribute handling of current state of the art graph transformation implementations. We show that our proposed approach preserves the fundamental theoretical results of the algebraic approach for graph transformations. Additionally, we verify the well-known results for the static verification of consistency constraints, conflict detection, and conflict resolution by confluence analysis within our framework. Finally, a prototypical implementation is provided to show that the theoretical concepts can be realized. Moreover, to assess its potential for analyzing real world applications, the prototype is applied to analyze a case study from the enterprise modeling domain