The OMG QVT standard aims at consolidating and simplifying the model transformation landscape
by offering three domain-specific languages (Relations, Operational Mappings, and Core)
inspired in the declarative and imperative paradigms. We focus on QVT-Relations,
which allows declaring a transformation as a set of relations that should hold between concrete models.
The standard states the well-formedness rules for QVT-Relations in English.
We provide instead an OCL formulation, thus formalizing the static semantics of the
language and allowing checking Abstract Syntax Trees (ASTs) before transformations take place.
Additionally, we express the dynamic semantics of QVT-Relations in Relational Logic.
With that, symbolic analyses (input coverage, output well-formedness) become possible
with the Alloy model-checker, allowing the design-time certification of transformations
with more reliable techniques than testing. A case-study confirms the practical benefits of the approach.