On verifying ATL transformations using ‘off-the-shelf’ SMT solvers

(post by Fabian Büttner) Recently, at this year’s MODELS conference, we (Fabian, myself and Marina Egea) have presented first results on the verification of ATL transformations using SMT solvers. In a nutshell, our approach allows us to verify that a declarative ATL transformation establishes all intended structural properties (i.e., transformation post-conditions, specified as OCL invariants) for the output metamodel. In short, we want to make sure the transformation always produce valid output models when applied on valid input models.

Technically, our approach consists of two steps:

1. We first automatically derive a first-order logic (FOL) specification from the ATL transformation and the OCL constraints that we want to consider on the input and output metamodels. That is, we generate a signature of predicates and functions and a set of logical assertions over them.
2. Then we use an SMT solver (we prefer Microsoft Z3) to check the properties. For each post-condition, we check whether the construction of a counter example is unfeasible.

In general, we generate a FOL specification that can represent models of arbitrary size. This means that we can conduct unbounded proofs for transformation correctness. As OCL, being part of the transformation, is known to be generally undecidable, the ATL verification problem is generally undecidable, too. However, for the case studies we have conducted so far (database schema transformations, state machine transformations), the Z3 solver could automatically prove all valid transformation properties fully automatically in less than a minute.

If you are interested in this line of research, please check out our MODELS paper or the slides of our presentation (below). All SMT files for Z3 (and, alternatively, for the Yices solver) are available online.