Expressive Symbolic-Execution Contract Proving for the DSLTrans Transformation Language

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

(2017-01)

September 2017

Zusammenfassung

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

Url: https://www.cs.mcgill.ca/media/tech_reports/None_Expressive_Symbolic-Execution_Contract_Proving_for_the_DSLTrans_Transf_Lky5uCT.pdf