Reference : Formal verification techniques for model transformations: A tridimensional classification
Scientific journals : Article
Engineering, computing & technology : Computer science
http://hdl.handle.net/10993/25157
Formal verification techniques for model transformations: A tridimensional classification
-
Amrani, M. [University of Luxembourg, Luxembourg]
Combemale, B. [University of Rennes 1, Inria, France]
Lúcio, L. [McGill University, Canada]
Selim, G. M. K. [Queen's University, Canada]
Dingel, J. [Queen's University, Canada]
Le Traon, Yves mailto [University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)]
Vangheluwe, H. [McGill University, Canada, University of Antwerp, Belgium]
Cordy, J. R. [Queen's University, Canada]
2015
Journal of Object Technology
Association Internationale pour les Technologies Objets
14
3
Yes (verified by ORBilu)
International
16601769
[en] Classification ; Formal verification ; Model transformation ; Model transformation intent ; Model-driven engineering ; Property of interest ; Survey ; Transformation languages
[en] 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.
NSERC, Natural Sciences and Engineering Research Council of Canada
http://hdl.handle.net/10993/25157
10.5381/jot.2015.14.3.a1

File(s) associated to this reference

Fulltext file(s):

FileCommentaryVersionSizeAccess
Open access
Formal Verification Techniques.pdfPublisher postprint2.3 MBView/Open

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.