ECEASST Verification of Model Transformations

Abstract: With the increasing use of automatic transformations of models, the correctness of these transformations becomes an increasingly important issue. Es-pecially for model transformation generally defined using abstract description tech-niques like graph transformations or declarative relational specifications, however, establishing the soundness of those transformations by test-based approaches is not straight-forward. We show how formal verification of soundness conditions over such declarative relational style transformations can be performed using an inter-active theorem prover. The relational style allows a direct translation of transfor-mations as well as associated soundness conditions into corresponding axioms and theorems. Using the Isabelle theorem prover, the approach is demonstrated for a refactoring transformation and a connectedness soundness condition