Description and proof of property preservation of model transformations

Model transformations are heavily used in model evolution, refinement and refactorings. Model transformations are carried out against certain constraints to preserve certain properties of the models. During model evolution, model transformations should preserve system interfaces; during model refactoring, model transformations should preserve system behaviors. In order to prove that a software transformation satisfies transformation constraints, constraints should be formalized first. And in order to automate the proof, the process of the proof should be universal to be supported by algorithms. This paper proposes an approach for formalizing transformation constraints with graph productions. With the formalized constraints and software transformation rules, an algorithm is also proposed based on critical pair analyzing technologies to automatically prove whether a transformation rule satisfies a transformation constraint or not. The proposed approach is validated with a motivating example used throughout the paper.