Correct-by-Construction Synthesis of Model Transformations using Transformation Patterns

Model transformations are an essential part of model-based development approaches, such as Model-driven Architecture (MDA) and Model-driven Development (MDD). Model transformations are used to refine and abstract models, to re-express models in a new modelling language, and to analyse, refactor, compare and improve models. Therefore, the correctness of model transformations is critically important for successful application of model-based development: software developers should be able to rely upon the correct processing of their models by transformations in the same way that they rely upon compilers to produce correct executable versions of their programs. In this paper, we address this problem by defining standard structures for model transformation specifications and implementations, which serve as patterns and strategies for constructing a wide range of model transformations. These are incorporated into a tool-supported process which automatically synthesises implementations of model transformations from their specifications, these implementations are correct-by-construction with respect to their specifications.