4.4.2 Transformation de modèle M2T
Cette section présente la validation du modèle
Event-B conforme au méta-modèle Event-B et la transformation de
ce modèle vers un texte Event-B. Le principe d'extraction est
montré par la Figure 4.31. Pour y parvenir, nous avons utilisé
avec profit les outils Check pour la validation et Xpand pour la
transformation.
4.4.2.1 Présentation de la transformation
M2T
La Figure 4.31 suivante donne le contexte de notre programme
permettant la transformation de modèle Event-B vers texte Event-B.
FIGURE 4.30 - Schéma de transformation
de modèle Event-B vers texte Event-B
La transformation proposée comporte quatre
étapes. La première étape a pour objectif de créer
le méta-modèle Event-B. Puis, la deuxième étape
consiste à créer un template. Xpt pour générer le
code Event-B. Ensuite, la troisième a pour objectif de créer un
modèle XMI conforme au méta-modèle Event-B puis valider ce
modèle xmi conforme via OclInECore. Finalement, la quatrième
partie consiste à exécuter le générateur de code
(generateur.mwe).
page 82
4.4 Transformations de modèle ECore vers Event-B en
utilisant une approche IDM (Ingénierie Dirigée par les
Modèles).
La première et troisième partie sont
déjà faite dans la section précédente(le
méta-modèle Event-B est le méta-modèle cible de la
transformation M2M et le modèle XMI conforme au
méta-modèle Event-B qui est le résultat de la
transformation ECore vers Event-B).
4.4.2.2 Modèle Event-B en texte : Extraction via
Xpand
L'outil Xpand est intégré dans l'environnement
EMF. Il permet la génération de code en partant d'un
modèle. Ce dernier doit être conforme à un
méta-modèle comme nous l'avons déjà
mentionné. Un fichier templateXpand (d'extension .xpt) comporte des
instructions d'import qui servent à importer le
méta-modèle, de zéro ou plusieurs EXTENSION avec le
langage Xtend et d'un ou plusieurs blocks DEFINE.
~ IMPORT
L'instruction IMPORT nous permet d'importer notre
méta-modèle contenant les méta-classes et leurs attributs
pour les utiliser dans notre approche template. Dans notre cas c'est le
méta-modèle nommé «Event-B » qui va être
utilisé.
« IMPORT Event-B»
~ Bloc DEFINE Les lignes suivantes dans le
fichier de modèle servent à définir le modèle pour
le fichier « Invariant ».Nous commençons par le modèle
en spécifiant son nom (INVARIANTS).
La déclaration de `Invariant' se traduit par le code
suivant :
|
«DEFINE INVARIANTS FOR Invariant»
«IFname.trim().length !=0 predicat.trim().length !=0»
«this.name» : «this.predicat»
«ENDIF»
«ENDDEFINE»
|
~ Instruction FILE Nous utilisons « FILE
» pour spécifier le type et l'extension de fichier de sortie qui va
être générée. Le nom du fichier est obtenu par la
concaténation de l'attribut « name » de « context »
actuelle et la chaine littérale `.buc'.
page 83
4.4 Transformations de modèle ECore vers Event-B en
utilisant une approche IDM (Ingénierie Dirigée par les
Modèles).
«DEFINEContenuContextFORContext"
'FILEname + ".buc""
...
...
'ENDFILE"
'ENDDEFINE"
o Instruction EXPAND EXPAND invoque un autre
sous modèle avec le nom «
Contenucontext"(respectivement'Contenumachine").
Ce sous modèle sera appelé pour chaque
élément dans les champs attribut (de référence) de
méta-classe « Context » actuelle (respectivement
méta-classe « Machine »).
«DEFINEContenuContextFORContext"
'FILEname + ".buc""
Context
'name"
'EXPANDEXTENDSFOREACHextends"
'IF!sets.isEmpty"
SETS
'EXPANDSET SFOREACHsets"
'ENDIF"
'IF!constants.isEmpty"
CONSTANTS
'EXPANDCONSTANT SFOREACHconstants"
'ENDIF"
'IF!axioms.isEmpty"
'ENDIF"
END
'ENDFILE"
'ENDDEFINE"
page 84
4.4 Transformations de modèle ECore vers Event-B en
utilisant une approche IDM (Ingénierie Dirigée par les
Modèles).
On trouve la version complète des règles de
transformation « model to text via Xpand » dans l'annexe C.
| 
