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 semi-automatically 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.
%0 Journal Article
%1 cabot_verification_2010
%A Cabot, Jordi
%A Clarisó, Robert
%A Guerra, Esther
%A de Lara, Juan
%D 2010
%J Journal of Systems and Software
%K Development; Grammars; Graph Model-to-model Triple Verification and transformation; validation {Model-Driven} {OCL}; {QVT};
%N 2
%P 283--302
%R 10.1016/j.jss.2009.08.012
%T Verification and validation of declarative model-to-model transformations through invariants
%V 83
%X 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 semi-automatically 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.
@article{cabot_verification_2010,
abstract = {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 semi-automatically 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.}},
added-at = {2013-02-28T11:13:35.000+0100},
author = {Cabot, Jordi and Claris{\'o}, Robert and Guerra, Esther and de Lara, Juan},
biburl = {https://www.bibsonomy.org/bibtex/293272f34d1ddceda5c0473c4abeb855d/fritzsolms},
doi = {10.1016/j.jss.2009.08.012},
interhash = {aa4569191be0cca5c091025641a82aa0},
intrahash = {93272f34d1ddceda5c0473c4abeb855d},
issn = {0164-1212},
journal = {Journal of Systems and Software},
keywords = {Development; Grammars; Graph Model-to-model Triple Verification and transformation; validation {Model-Driven} {OCL}; {QVT};},
month = feb,
number = 2,
pages = {283--302},
timestamp = {2013-02-28T11:13:42.000+0100},
title = {{Verification and validation of declarative model-to-model transformations through invariants}},
volume = 83,
year = 2010
}