@techreport{, author = {Oakes, Bentley James and L{\'{u}}cio, Levi and Gomes, Cl{\'{a}}udio and Vangheluwe, Hans}, title = {Expressive Symbolic-Execution Contract Proving for the {DSLTrans} Transformation Language}, publisher = {McGill University, School of Computer Science}, number = {2017-01}, year = {2017}, month = sep, school = {McGill University, School of Computer Science}, abstract = {The verification of model transformations is key for the adoption of model-driven engineering in academic and industrial processes. In this work, we provide a verification technique for our model transformation language DSLTrans, which is both confluent and terminating by construction. This technique proves structural pre-condition/ post-condition structural contracts for all inputs to a transformation. This is achieved by creating path conditions for the transformation through a symbolic execution of the transformation’s rules. These path conditions then represent all possible transformation executions through an abstraction relation. In this work, we provide a detailed description of both the path condition construction and contract proving techniques. As well, we provide arguments that our techniques are valid, such that proving a contract on the finite set of path conditions for a transformation implies that the contract holds on the infinite set of abstracted transformation executions.}, keywords = {Model-based Systems Engineering, MbSE}, url = {https://www.cs.mcgill.ca/media/tech_reports/None_Expressive_Symbolic-Execution_Contract_Proving_for_the_DSLTrans_Transf_Lky5uCT.pdf}, }