A Visual Specification Language for Model-to-Model Transformations

Model Driven Engineering promotes models as the core assets of projects and hence model transformations become first-class citizens in this approach. Likewise, the development of large scale transformations necessitates a systematic engineering process and supporting modelling notations. However, although many languages have been proposed to implement transformations, few allow their specification at a higher level of abstraction. In this paper we present a visual, formal, declarative specification language to express model-to-model transformations and their correctness properties. The language supports the two main approaches to model-to-model transformation -- trace-based and traceless -- with a unified formal semantics. Moreover, we provide a compilation of specifications into OCL as this has many practical applications, e.g. it allows injecting assertions and correctness properties for automated testing of transformation implementations based on OMG standards.