Uncovering Errors in ATL Model Transformations Using Static Analysis and Constraint Solving

Model transformations play a prominent role in Model-Driven Engineering (MDE), where they are used to transform models between languages, to refactor and simulate models, or to generate code from models. However, while the reliability of any MDE process depends on the correctness of its transformations, methods helping in detecting errors in transformations and automate their verification are still needed. To improve this situation, we propose a method for the static analysis of one of the most widely used model transformation languages: ATL. The method proceeds in three steps. Firstly, it infers typing information from the transformation and detects potential errors statically. Then, it generates OCL path conditions for the candidate errors, stating the requirements for a model to hit the problematic statements in the transformation. Last, it relies on constraint solving to generate a test model fragment or witness that exercises the transformation, making it execute the problematic statement. Our method is supported by a prototype tool that integrates a static analyzer, a testing tool and a constraint solver. We have used the tool to analyse medium and large-size third-party ATL transformations, discovering a wide number of errors.