Verification and Validation of Declarative Model-to-Model Transformations through Invariants Articles uri icon

authors

  • CABOT, JORDI
  • CLARISO, ROBERT
  • GUERRA SANCHEZ, ESTHER
  • DE LARA, JUAN

publication date

  • March 2010

start page

  • 283

end page

  • 302

issue

  • 2

volume

  • 83

International Standard Serial Number (ISSN)

  • 0164-1212

Electronic International Standard Serial Number (EISSN)

  • 1873-1228

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.