Affordable Access

Publisher Website

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

Authors
Journal
Journal of Systems and Software
0164-1212
Publisher
Elsevier
Publication Date
Volume
83
Issue
2
Identifiers
DOI: 10.1016/j.jss.2009.08.012
Keywords
  • Model-To-Model Transformation
  • Model-Driven Development
  • Ocl
  • Verification And Validation
  • Triple Graph Grammars
  • Qvt

Abstract

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.

There are no comments yet on this publication. Be the first to share your thoughts.