Semantical correctness and completeness of model transformations using graph and rule transformation. (English) Zbl 1175.68221

Ehrig, Hartmut (ed.) et al., Graph transformations. 4th international conference, ICGT 2008, Leicester, United Kingdom, September 7–13, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-87404-1/pbk). Lecture Notes in Computer Science 5214, 194-210 (2008).
Summary: 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 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.
For the entire collection see [Zbl 1148.68002].


68Q42 Grammars and rewriting systems
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Full Text: DOI Link