TY - JOUR
T1 - Formal verification techniques for model transformations
T2 - A tridimensional classification
AU - Amrani, Moussa
AU - Combemale, Benoît
AU - Lúcio, Levi
AU - Selim, Gehan M.K.
AU - Dingel, Jürgen
AU - Le Traon, Yves
AU - Vangheluwe, Hans
AU - Cordy, James R.
PY - 2015
Y1 - 2015
N2 - In Model Driven Engineering (Mde), models are first-class citizens, and model transformation is Mde's "heart and soul". Since model transformations are executed for a family of (conforming) models, their validity becomes a crucial issue. This paper proposes to explore the question of the formal verification of model transformation properties through a tridimensional approach: the transformation involved, the properties of interest addressed, and the formal verification techniques used to establish the properties. This work is intended for a double audience. For newcomers, it provides a tutorial introduction to the field of formal verification of model transformations. For readers more familiar with formal methods and model transformations, it proposes a literature review (although not systematic) of the contributions of the field. Overall, this work allows to better understand the evolution, trends and current practice in the domain of model transformation verification. This work opens an interesting research line for building an engineering of model transformation verification guided by the notion of model transformation intent.
AB - In Model Driven Engineering (Mde), models are first-class citizens, and model transformation is Mde's "heart and soul". Since model transformations are executed for a family of (conforming) models, their validity becomes a crucial issue. This paper proposes to explore the question of the formal verification of model transformation properties through a tridimensional approach: the transformation involved, the properties of interest addressed, and the formal verification techniques used to establish the properties. This work is intended for a double audience. For newcomers, it provides a tutorial introduction to the field of formal verification of model transformations. For readers more familiar with formal methods and model transformations, it proposes a literature review (although not systematic) of the contributions of the field. Overall, this work allows to better understand the evolution, trends and current practice in the domain of model transformation verification. This work opens an interesting research line for building an engineering of model transformation verification guided by the notion of model transformation intent.
KW - Classification
KW - Formal verification
KW - Model transformation
KW - Model transformation intent
KW - Model-driven engineering
KW - Property of interest
KW - Survey
KW - Transformation languages
UR - http://www.scopus.com/inward/record.url?scp=84944112108&partnerID=8YFLogxK
U2 - 10.5381/jot.2015.14.3.a1
DO - 10.5381/jot.2015.14.3.a1
M3 - Article
AN - SCOPUS:84944112108
SN - 1660-1769
VL - 14
JO - Journal of Object Technology
JF - Journal of Object Technology
IS - 3
ER -