Automated verification of model transformations based on visual contracts
Sprache des Titels:
Model-Driven Engineering promotes the use of models to conduct the different
phases of the software development. In this way, models are transformed between
different languages and notations until code is generated for the final application. Hence, the construction of correct Model-to-Model (M2M) transformations
becomes a crucial aspect in this approach.
Even though many languages and tools have been proposed to build and execute
M2M transformations, there is scarce support to specify correctness requirements for
such transformations in an implementation-independent way, i.e., irrespective of the
actual transformation language used.
In this paper we fill this gap by proposing a declarative language for the specification
of visual contracts, enabling the verification of transformations defined with any
transformation language. The verification is performed by compiling the contracts
into QVT to detect disconformities of transformation results with respect to the contracts.
As a proof of concept, we also report on a graphical modeling environment for
the specification of contracts, and on its use for the verification of transformations in
several case studies.