The research area of graph grammars or graph transformations is a discipline of computer science which dates back to the 1970s. Methods, techniques, and results from this area have already been studied and applied in many fields of computer science, such as formal language theory, pattern recognition, the modeling of concurrent and distributed systems, database design and theory, logical and functional programming, model and program transformation, syntax and semantics of visual languages, refactoring of programs and software systems, process algebras, and Petri nets. This wide applicability is due to the fact that graphs are a very natural way of explaining complex situations on an intuitive level. Hence, they are used in computer science almost everywhere.
The concept of model transformations is of increasing importance in software engineering, especially in the context of model-driven development. Although many model transformation approaches are implemented in various tools and utilized by a wide range users, often these implementations are quite ad-hoc and without any proven correctness. Thus, in the last years the need for analysis and verification of model transformations has emerged. As a basis, a formal framework is needed which allows to obtain respective results. In this thesis, we use graph transformation to define model transformations and verify certain correctness properties. In this chapter, the basic concepts of graph and model transformations are introduced and a survey of recent literature is given.
M -adhesive categories constitute a powerful framework for the definition of transformations. The double–pushout approach, which is based on categorical constructions, is a suitable description of transformations leading to a great number of results as the Local Church-Rosser, Parallelism, Concurrency, Embedding, Extension, and Local Confluence Theorems. Yet the rules and transformations themselves are easy and intuitively to understand.
In this chapter, we introduce amalgamated transformations, which are useful for the definition of the semantics of models using transformations. An amalgamated rule is based on a kernel rule, which defines a fixed part of the match, and multi rules, which extend this fixed match. From a kernel and a multi rule, a complement rule can be constructed which characterizes the effect of the multi rule exceeding the kernel rule. An interaction scheme is defined by a kernel rule and available multi rules, leading to a bundle of multi rules that specifies in addition how often each multi rule is applied. Amalgamated rules are in general standard rules in M -adhesive transformation systems, thus all the results follow. In addition, we are able to refine parallel independence of amalgamated rules based on the induced multi rules. If we extend an interaction scheme as large as possible we can describe the transformation for an unknown number of matches, which otherwise would have to be defined by an infinite number of rules. This leads to maximal matchings, which are useful to define the semantics of models.
Triple graphs and triple graph grammars are a successful approach to describe model transformations. They relate the source and target models by some connection parts thereby integrating both models into one graph. This uniform description of both models allows to obtain a unified theory for forward and backward transformations.
Model transformations from a source to a target language can be described by triple graph transformations as shown in Chapter 5. Important properties for the analysis and correctness of such model transformations are syntactical correctness, completeness, and functional behavior. Moreover, the semantics of the source and target models may be given by interaction schemes using amalgamation as done in Chapter 4. In this case, we are interested in analyzing the semantical correctness, i. e. the correctness of the model transformation with respect to the semantical behavior of the corresponding source and target models.
Graphs are a very natural way to explain complex situations on an intuitive level. Hence, they are useful for the visual specification of systems. Nevertheless, it is still complicated to combine an easy, intuitive approach with a formal description leading to a wide range of analysis techniques for complex structures. Graph transformation with its formal background in category theory and its broad theoretical results concerning the behavior of models constitutes a suitable foundation for the description of system behavior and model transformations.
Ulrike Golas
Backmatter
Metadaten
Titel
Analysis and Correctness of Algebraic Graph and Model Transformations
