Verification of the CD2RDBMS Transformation Case in Flora-2.
Muzaffar Igamberdiev, Georg Großmann, Markus Stumptner · 2015
Model transformations play a key role in model-driven development. They are used to generate, refactor, synthesize, reverse engineer and simplify models among others. The accuracy of transformations will impact not only transformations themselves, but also the models, the first class entities of MDE. Verification of correctness properties ensures the quality of both transformations and models. VOLT workshop has been addressing this important research area for several years. As a solution for the VOLT-2015 case on transformation between class diagrams and RDBMS models, we provide a verification approach, namely MOTIF, in Flora-2 language. By specifying models, transformations and verification in the same language, we aim at closing the research gap between models and verification formalism.