Scalable verification of model transformations

Abstract

Model transformations are crucial in model driven engineering (MDE). Automatic execution of model transformations improves software development productivity. However, model transformations should be verified to ensure that the models produced or the transformations satisfy some expected properties. In a previous work we presented a verification approach of graph-based model transformation systems based on relational logic. The approach encodes model transformation systems as Alloy specifications which are examined by the Alloy Analyzer. But experiments showed scalability and performance problems in the approach when complex relations were present in the systems. To solve these problems, we extend our previous work by using three techniques: 1) we change the encoding to decrease the arity of relations in the derived Alloy specifications; 2) we decompose the expressions for the pattern matching into sub-expressions using unique elements; 3) we use annotations to decrease the complexity of the metamodel and the model transformation rules. The results of our experiments indicate that the new techniques lead to better scalability and performance.