Verification and validation of declarative model-to-model transformations through invariants

In this paper we propose a method to derive OCL invariants from declarative model-to-model transformations in order to enable their verification and analysis. For this purpose we have defined a number of invariant-based verification properties which provide increasing degrees of confidence about transformation correctness, such as whether a rule (or the whole transformation) is satisfiable by some model, executable or total. We also provide some heuristics for generating meaningful scenarios that can be used to semiautomatically validate the transformations. As a proof of concept, the method is instantiated for two prominent model-to-model transformation languages: Triple Graph Grammars and QVT. Key words: Model-to-Model Transformation, Model-Driven Development, OCL, Verification and Validation, Triple Graph Grammars, QVT

• Type: Journal
• Year: 2010
• Where: JSS
• Authors: Jordi Cabot, Robert Clarisó, Esther Guerra, Juan de Lara
• Keywords: Invariant-based Verification Properties, JSS 2010, Model-to-model Transformation, Triple Graph Grammars