Model-Driven Engineering (MDE) has emerged as a new paradigm which uses models as the main artifacts in the development process. Model transformations are the heart and soul of MDE, such that software is automatically generated from the models via applying transformations. Model transformations are defined using transformation languages. During the last decade, different transformation languages have been introduced to the model-driven community. Since the correctness of a transformation has a direct impact on generating the final product, verification of a model transformation is an important issue. Epsilon Transformation Language (ETL) is one of the most widely used model transformation languages across the community. Few studies have addressed the verification of ETL transformations. These studies have several limitations as follows: less attention to the transformation definition, lack of fully automatic tool, no reasoning about the correctness of output and considering a specific input model.
In this research, using symbolic execution technique, two approaches are proposed in order to detect logical errors in ETL transformations. The first approach is using an indirect approach. That means, it transforms the ETL transformation to DSLTrans, so that using the SyVOLT tool it is possible to symbolically execute the DSLTrans transformation and indirectly conduct contract verification of the transformation. The second approach applies a direct approach, called SEET, for symbolic execution of ETL transformations. It generates symbolic output model which can be used to detect logical errors in ETL transformations. SEET is integrated as an Eclipse plugin. The proposed approaches are input-independent. The experimental results show the superiority of the proposed approaches to detect logical errors in ETL transformations.