Specification and verification of graph-based model transformation properties

Abstract

We extend a previously proposed symbolic model transformation property prover for the DSLTrans transformation language. The original prover generated the set of path conditions (i.e., symbolic transformation executions), and verified atomic contracts (constraints on input-output model relations) on these path conditions. The prover evaluated atomic contracts to yield either true or false for the transformation when run on any input model. In this paper we extend the prover such that it can verify atomic contracts and more complex properties composed of atomic contracts. Besides demonstrating our prover on a simple transformation, we use it to verify different kinds of properties of an industrial transformation. Experiments on this transformation using our prover show a speed-up in verification run-time by two orders of magnitude over another verification tool that we evaluated in previous research. © 2014 Springer International Publishing Switzerland.