Semantical Correctness and Completeness of Model Transformations using Graph and Rule Transformation: Long Version

An important requirement of model transformations is the preservation of the behavior of the original model. A model transformation is semantically correct if for each simulation run of the source system we find a corresponding simulation run in the target system. Analogously, we have semantical completeness, if for each simulation run of the target system we find a corresponding simulation run in the source system. In our framework of graph transformation, models are given by graphs, and graph transformation rules are used to define the operational behavior of visual models (called simulation rules). In order to compare the semantics of source and target models, we assume that in both cases operational behavior can be defined by simulation rules. The model transformation from source to target models is given by another set of graph transformation rules. These rules are also applied to the simulation rules of the source model. The result of this rule transformation is compared with the given simulation rules of the target language.The main result in this paper states the conditions for model and rule transformations to be semantically correct and complete. The result is applied to analyze the behavior of a model transformation from a domain-specific visual language for production systems to Petri nets