Formal Verification Techniques for Model Transformations: A Tridimensional Classification

Abstract : 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.
Type de document :
Article dans une revue
The Journal of Object Technology, Chair of Software Engineering, 2015, 14 (3), pp.1:1-43. 〈http://www.jot.fm/contents/issue_2015_03/article1.html〉. 〈10.5381/jot.2015.14.3.a1〉
Liste complète des métadonnées

Littérature citée [119 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01083759
Contributeur : Benoit Combemale <>
Soumis le : mardi 18 novembre 2014 - 16:07:16
Dernière modification le : mercredi 2 août 2017 - 10:09:00
Document(s) archivé(s) le : jeudi 19 février 2015 - 14:55:33

Fichier

JoT2014-final.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité - Pas d'utilisation commerciale - Pas de modification 4.0 International License

Identifiants

Citation

Moussa Amrani, Benoît Combemale, Levi Lúcio, Gehan Selim, Jürgen Dingel, et al.. Formal Verification Techniques for Model Transformations: A Tridimensional Classification. The Journal of Object Technology, Chair of Software Engineering, 2015, 14 (3), pp.1:1-43. 〈http://www.jot.fm/contents/issue_2015_03/article1.html〉. 〈10.5381/jot.2015.14.3.a1〉. 〈hal-01083759〉

Partager

Métriques

Consultations de
la notice

776

Téléchargements du document

571