A rigorous reasoning about model transformations using the B method

Akram Idani 1 Yves Ledru 1 Adil Anwar 2
1 VASCO
LIG - Laboratoire d'Informatique de Grenoble
Abstract : A crucial idea of Model Driven Engineering is that model transformation can be described uniformly in terms of meta-model mappings. Based on the fact that meta-models define an abstract syntax from which one can describe elements of modeling languages, transformation rules that arise from MDA-based techniques are often described as explicit and clear. However, one of the remaining difficulties is to check the correctness of these transformations in order to prove that they preserve constraints which may be expressed over meta-models. Currently, the MDE gives methodological issues for the use of OCL to express these constraints but without providing automated formal reasonings. This paper discusses how a formal method, such as B, can be used in an MDE process in order to rigourously reason about meta-models and associated model transformations. We propose to adapt existing UML-to-B techniques in order to obtain a formal specification of meta-models and hence the various constraints can be introduced using B invariants. We also show how transformation rules can be encoded using B operations and what kinds of reasoning can be performed on the resulting B specifications. Such a technique allows to assist the MDE by proof and animation tools.
Type de document :
Communication dans un congrès
Selmin Nurcan et al. EMMSAD 2013 - International Conference on Exploring Modelling Methods for Systems Analysis and Design (held at CAiSE 2013), Jun 2013, Valencia, Spain. Springer, 147, pp.426-440, 2013, Lecture Notes in Business Information Processing (LNBIP). 〈10.1007/978-3-642-38484-4_30〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00853720
Contributeur : Akram Idani <>
Soumis le : vendredi 23 août 2013 - 15:50:07
Dernière modification le : mardi 28 octobre 2014 - 18:33:32

Identifiants

Collections

Citation

Akram Idani, Yves Ledru, Adil Anwar. A rigorous reasoning about model transformations using the B method. Selmin Nurcan et al. EMMSAD 2013 - International Conference on Exploring Modelling Methods for Systems Analysis and Design (held at CAiSE 2013), Jun 2013, Valencia, Spain. Springer, 147, pp.426-440, 2013, Lecture Notes in Business Information Processing (LNBIP). 〈10.1007/978-3-642-38484-4_30〉. 〈hal-00853720〉

Partager

Métriques

Consultations de la notice

215