Formal Semantics of Consistent EMF Model Transformations by Algebraic Graph Transformation

Model transformation is one of the key activities in model-driven software development. An increasingly popular technology to define mod-eling languages is provided by the Eclipse Modeling Framework (EMF). Several EMF model transformation approaches have been developed, focus-ing on different transformation aspects. To validate model transformations wrt. functional behavior and correctness, a formal foundation is needed. In this paper, we define EMF model transformations as a special kind of typed graph transformations using node type inheritance. Containment con-straints of EMF model transformations are translated to a special kind of EMF model transformation rules such that their application leads to con-sistent transformation results only. Thus, we identify a kind of EMF model transformations which behave like algebraic graph transformations. As a consequence, the rich theory of algebraic graph transformation can be ap-plied to these EMF model transformations to show functional behavior and correctness. Furthermore, we propose parallel graph transformation as a suitable framework for modeling EMF model transformations with multi-object structures. Multi-object structures at transformation rule level pro-vide a flexible way to describe the transformation of structures with a flexi-ble number of recurring structures, dependent on concrete model instances. Parallel graph transformation means parallelizing the application of model transformation rules at several occurences at once. We illustrate our ap-proach by selected refactorings of simplified statechart models. Finally, we discuss the implementation of our concepts in a tool environment for EMF model transformations