4.4 Transformations de modèle ECore vers Event-B
en utilisant une approche IDM (Ingénierie Dirigée par les
Modèles).
Dans cette section, nous proposons une approche et un outil
pour la transformation de modèle ECore vers Event-B en utilisant une
approche IDM (Ingénierie Dirigée par les Modèles). Notre
approche est basée sur la transformation de modèles. Le
résultat de la transformation (code Event-B) sera ensuite
l'entrée de l'outil RODIN pour vérifier la cohérence et la
fiabilité du modèle Event-B obtenu.
Notre approche suit le schéma suivant :
FIGURE 4.20 - Schéma de notre
approche
Le passage des modèles ECore vers leurs
équivalents en Event-B a été réalisé par une
transformation de modèle en utilisant une approche IDM. Cette
transformation est réalisée sous l'environnement de programmation
Java Eclipse en utilisant ATL comme langage de transformation M2M et Xpand pour
la transformation M2T. Les modèles ECore et Event-B sont
réalisés en conformité avec leurs
méta-modèles respectifs.
page 71
4.4 Transformations de modèle ECore vers Event-B en
utilisant une approche IDM (Ingénierie Dirigée par les
Modèles).
4.4.1 Transformation de modèles M2M
Nous allons présenter les règles de
transformation permettant le passage d'un modèle ECore vers un
modèle Event-B. Ces règles sont établies entre le
méta-modèle source et le méta-modèle cible,
autrement dit entre tous les concepts des méta-modèles source et
cible. Ces règles sont expliquées brièvement suivant en
langage naturel.
Après la présentation des règles de
transformation, maintenant nous allons définir quelques règles en
utilisant ATL comme langage de transformation d'un modèle ECore en un
modèle Event-B.
La Figure 4.22 donne le contexte de notre programme
ECore2Event-B permettant de transformer une modélisation ECore vers une
spécification Event-B.
page 72
4.4 Transformations de modèle ECore vers Event-B en
utilisant une approche IDM (Ingénierie Dirigée par les
Modèles).
FIGURE 4.21 - Vue d'ensemble sur le programme ECore2Event-B
Les modèles source et cible (modélisation en
ECore et spécification en Event-B) ainsi que le programme ECore2Event-B
sont conformes à leurs méta-modèles ECore, Event-B et ATL.
Dans un premier temps, nous avons développé deux modèles
correspondant aux méta-modèles source ECore et cible Event-B. Ces
méta-modèles sont conformes au
méta-méta-modèle ECore.
L'entête du programme ECore2Event-B stockée dans
le fichier ECore2Event-B.atl se présente comme suit :
module ECore2Event-B;
create modeleEvent-B: Event-B modeleECore : ECore
Dans notre programme le modèle cible est
représenté par la variable modèle Event-B à partir
du modèle source représenté par modeleECore.
Les modèles source et cible sont respectivement
conformes aux méta-modèles ECore et Event-B. Notre programme
ECore2Event-B opère sur le modèle source modeleECore en lecture
seule et produit le modèle cible modèle Event-B en
écriture seule.
page 73
4.4 Transformations de modèle ECore vers Event-B en
utilisant une approche IDM (Ingénierie Dirigée par les
Modèles).
4.4.1.1 Exemple des règles en ATL
Avant de commencer à définir des règles de
transformation, nous allons donner la forme générale de celles-ci
dans la Figure 4.23 :
ruleForExample {
from
i :inputMetamodel !InputElement
to
a :OutputMetaModel !OutputElement (
attributeA<-i.attributeA,
attributeB<-i.attributeC
)}
FIGURE 4.22 - Exemple règle ATL
~ Forexample : est le nom de la règle de
transformation.
~ I (resp. O) : est le nom de la variable représentant
la source d'élément identifié que, dans le corps de la
règle (resp. élément cible créé).
~ InputMetaModel (resp. OutputMetaModel) : est le
méta-modèle dans lequel le modèle de source (resp. le
modèle de cible) de la transformation est constante.
~ InputElement : signifie la méta-classe
d'éléments de modèle de source à laquelle cette
règle sera appliquée.
~ OutputElement : signifie la méta-classe à
partir de laquelle la règle instancie les éléments
cibles.
~ Le point d'exclamation! : est utilisé pour
spécifier à quel méta-modèle appartient une classe
méta.
~ AttributeA et attributeB : sont des attributs de la
méta-classe OutputElement, leurs valeurs sont initialisées
à l'aide des valeurs des attributs i.attributeA, i.attributeCde
l'InputElement.
Après la présentation des règles de
transformation, maintenant nous allons définir quelques règles en
utilisant ATL comme langage de transformation d'un modèle ECore en un
modèle Event-B.
page 74
4.4 Transformations de modèle ECore vers Event-B en
utilisant une approche IDM (Ingénierie Dirigée par les
Modèles).
Règle générant Context et
Machine
Reprenons l'exemple de la Règle qui transforme un
EPackage ECore en CONTEXT Event-B et aussi en MACHINE Event-B. Le
résultat de cette transformation est montré dans la Figure
4.24.
2
4
6
8
10
12
14
16
18
20
22
24
rule EPackage2RootContextMachine
{ from z :MM! EPackage
to
a :MM1!ROOT (
contextes<-Sequence {ctx } ,
contextes <-Sequence {mch}) , ctx : MM1! Context
(
name<- z . name+' ctx ',
sets <-z . eC la s si f ie rs ->select ( el | el .
oclIsTypeOf (MM! EClass ) ) , sets <-z . eC la s si f ie rs ->select ( el
| el . oclIsTypeOf (MM!EEnum) ) ,
constants <- Sequence {thisModule . GetEEnumLiteral1->c
o l l e c t ( e | thisModule . resolveTemp (e , ' const1 ' ) ) } ,
constants <- Sequence
axioms <- Sequence {thisModule . GetEReference1->c o l l e
c t
( e | thisModule . resolveTemp (e , ' f f ' ) )} ) ,
mch : MM1! Machine ( name <- z . name+'M' ,
variables <-Sequence{thisModule . GetEClass1 ->collect (
e | thisModule . resolveTemp
(e , ' const4 ' ) )}
. . . .
)}
Voici la règle écrite en ATL.
page 75
3
5
7
9
11
13
3
5
7
3
5
7
9
11
13
23
25
27
4.4 Transformations de modèle ECore vers Event-B en
utilisant une approche IDM (Ingénierie Dirigée par les
Modèles).
FIGURE 4.23 - Règle générant Context et
Machine
Règle générant les ensembles
abstraits(Sets)
2
4
6
8
10
12
14
16
Reprenons l'exemple de la Règle qui transforme le concept
EClass en « EVENT » dans MACHINE Event-B. Le résultat de cette
transformation est montré dans la Figure 4.25. Voici la règle
écrite en ATL.
|
rule EClass2Sets {
from cc : MM! EClass
to const3 : MM1! Sets (
name <- cc . name . firstToLower ()
) ,
const4 : MM1! Variable (
name <- cc . instanceClassName ) ,
inv : MM1! Invariant (
name <-' inv0 ' ,
predicat <-cc . instanceClassName+'IN '+cc . name ) ,
i n it :MM1! Event (
name <- 'INITIALISATION' ,
actions <-Sequence{ action2 }
) ,
action2 : MM1! Action (
name <-' act ',
predicat <-cc . instanceClassName+' := '+'empty' ) }
|
page 76
4.4 Transformations de modèle ECore vers Event-B en
utilisant une approche IDM (Ingénierie Dirigée par les
Modèles).
FIGURE 4.24 - Règle générant Sets
Règle générant les
événements (Event)
Reprenons l'exemple de la Règle qui transforme le
concept EOperation en « EVENT » dans MACHINE Event-B. Le
résultat de cette transformation est montré dans la Figure
4.26.
1
Ci-dessous la règle écrite en ATL.
|
rule Eoperation2Event {
from
H: MM! EOperation
Toevt : MM1! Event (
name <- H. name,
parameters <-H. eParameters ,
guards <- Sequence {thisModule . allMethodDefsprm->
collect ( e | thisModule . resolveTemp (e , ' grd ' ) ) }) }
rule EParameter2ParameterAndGuard {
from
Z: MM! EParameter
to
ZZ: MM1! Parameter (
name <- Z. name
|
15
17
page 77
4.4 Transformations de modèle ECore vers Event-B en
utilisant une approche IDM (Ingénierie Dirigée par les
Modèles).
|
) ,
grd : MM1! Guard (
name <- ' gdr1 ',
predicat<-Z. name+' '+'IN '+' '+Z. eType . name)}
|
FIGURE 4.25 - Règle générant Event
Règle générant les Constants
(Constants)
1
Reprenons l'exemple de la Règle qui transforme le concept
EEnumLiteral en « Constants » dans Context Event-B. Le
résultat de cette transformation est montré dans la Figure 4.27.
Ci-après la règle écrite en ATL.
|
rule EEnumLiteral2ConstantsAndAxioms {
from
EnumLiteral : MM! EEnumLiteral
to
const1 : MM1! Constants (
name <- EnumLiteral . name
) ,
const2 :MM1! Axioms (
|
9
11
page 78
4.4 Transformations de modèle ECore vers Event-B en
utilisant une approche IDM (Ingénierie Dirigée par les
Modèles).
|
name <- 'axm1-1 ',
predicat <-'PARTITION '+' '+' ( '+EnumLiteral . eEnum. name
+','+'{ '+EnumLiteral . name+'} '+' ) ' ) }
|
FIGURE 4.26 - Règle générant Constants
Règle générant les ensembles
(Sets)
1
Reprenons l'exemple de la Règle qui transforme le concept
EEnum en « SETS » dans CONTEXT Event-B. Le résultat de cette
transformation est montré dans la Figure 4.28. Ci-dessous la
règle écrite en ATL.
|
rule EEnum2Sets {
from
Enum: MM!EEnum
to
sets: MM1! Sets (
name <- Enum. name
) ,
enum : MM1! Variable (
name <- Enum. instanceClassName
) ,
inv1 : MM1! Invariant (
name <-' inv0 ' ,
predicat <-Enum. instanceClassName+'IN '+Enum. name
) ,
|
15
17
19
21
page 79
4.4 Transformations de modèle ECore vers Event-B en
utilisant une approche IDM (Ingénierie Dirigée par les
Modèles).
init1 :MM1! Event (
name <- 'INITIALISATION' ,
actions <-Sequence{ action1 }
) ,
action1 : MM1! Action (
name <-' act ',
predicat <-Enum. instanceClassName+':= '+' isEmpty () '
)
actions <-Sequence{ action3 } ) ,
action3 : MM1! Action (
name <-' act ',
predicat <-a . name+':= '+' isEmpty () '
)}
FIGURE 4.27 - Règle générant Sets
L'annexe C présente le reste des règles de
transformation « .atl ». 4.4.1.2 Exécution du
programme ECore2Event-B.atl
Le moteur de transformation permet de générer le
modèle Event-B, ce qui est conforme au méta-modèle
Event-B, à partir du modèle ECore qui est conforme au
méta-modèle ECore en utilisant le programme ECore2Event-B.atl,
qui doit être également conforme au méta-modèle qui
définit la sémantique de la transformation ATL. Tous les
méta-modèles doivent être conformes à la
méta-méta-modèle ECore.
Pour valider nos règles de transformation, nous avons
réalisé un test. A titre d'illustration,
4.4 Transformations de modèle ECore vers Event-B en
utilisant une approche IDM (Ingénierie Dirigée par les
Modèles).
nous considérons l'exemple d'un compte bancaire
présenté dans le chapitre 2. (Voir Figure 4.29).
FIGURE 4.28 - Modèle ECore d'un Bank (modèle
source)
Lorsque le modèle est validé et il n'y a pas
d'erreurs, et après l'ajout des contraintes OCL attachées au
modèle, l'utilisateur peut exécuter le programme de
transformation de modèle ATL pour transformer le modèle ECore en
Event-B. Le résultat de cette transformation est
représenté sur la Figure 4.30 ci-dessous.
page 80
FIGURE 4.29 - Modèle Event-B d'un Bank (modèle
cible)
page 81
4.4 Transformations de modèle ECore vers Event-B en
utilisant une approche IDM (Ingénierie Dirigée par les
Modèles).
| 
