Expressive Symbolic-Execution Contract Proving for the DSLTrans Transformation Language

Bentley James Oakes, Levi Lúcio, Cláudio Gomes und Hans Vangheluwe


September 2017


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.

Stichworte: Model-based Systems Engineering, MbSE