Checking model transformation refinement

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-642-38883-5_15Proceedings of 6th International Conference, ICMT 2013, Budapest, Hungary, June 18-19, 2013Refinement is a central notion in computer science, meaning that some artefact S can be safely replaced by a refinement R, which preserves S’s properties. Having available techniques and tools to check transformation refinement would enable (a) the reasoning on whether a transformation correctly implements some requirements, (b) whether a transformation implementation can be safely replaced by another one (e.g. when migrating from QVT-R to ATL), and (c) bring techniques from stepwise refinement for the engineering of model transformations. In this paper, we propose an automated methodology and tool support to check transformation refinement. Our procedure admits heterogeneous specification (e.g. PaMoMo, Tracts, OCL) and implementation languages (e.g. ATL, QVT), relying on their translation to OCL as a common representation formalism and on the use of model finding tools.Research partially funded by the Nouvelles Equipes ´Program of the Pays de la Loire Region (France), the EU project NESSoS (FP7 256890), the Spanish Ministry of Economy and Competitivity (project “Go Lite” TIN2011-24139), the R&D programme of the Madrid Region (project “e-Madrid” S2009/TIC-1650