An approach based on Z language for formalization of model transformation definition

Abstract

The creation of transformation definition is an important step in the process of model transformation in the context of Model Driven Engineering. However, the manual creation of transformation definition is vulnerable to ambiguity due to miss interpretation of the metamodels and their relationships or due to human factors like fatigue. In this paper, we propose an approach based on the Z formal language for specifying the transformation definition. Firstly, transformation rules are specified in Z language, and then validated by a testing tool called Z/EVES that supports statements in first-order predicate logic and set theory. Afterwards, the formalism in Z is translated in a transformation language such as ATL. An illustrative example is provided in order to demonstrate our approach. © 2013 Springer Science+Business Media.