4.2.2 Méta-modèle ECore
Le méta-modèle ECore utilisé comme
méta-modèle source pour notre approche de transformation de ECore
vers Event-B est donné par la Figure 4.10 (sous forme du diagramme) et
par la Figure 4.11 (Méta-modèle ECore ouvert avec son
éditeur).
page 60
4.2 Les méta-modèles de notre approche
FIGURE 4.10 - Méta-modèle
ECore ouvert avec son éditeur
page 61
4.2 Les méta-modèles de notre approche
FIGURE 4.11 - Méta-modèle
ECore partiel
page 62
4.2 Les méta-modèles de notre approche
4.2.2.1 Les règles de cohérence du
méta-modèle ECore sous forme d'OCL (OCLi-nECore)
Nous avons établi des propriétés
décrivant des contraintes d'utilisation d'ECore. De telles
propriétés sont décrites d'une façon informelle et
formelle en se servant d'OCL.
~ Propriété 1 :
Dans une même EClass une EOperation, un EAttribute et
une EReference doivent avoir des noms deux à deux différents.
Ceci, est formalisé en OCL comme suit et montré par la Figure
4.12 :
Invariant CheckNamesEClass:
eStructuralFeatures->collect(self
eStructuralFeatures->collect(name)) ->excludesAll(self
eOperations->collect(self eOperations->collect(name )));
FIGURE 4.12 - Règle sous forme d'OCLinECore.
En cas d'erreur un message sera affiché et
l'exécution sera arrêtée. Ceci est illustré par la
Figure 13 suivante :
page 63
4.3 Formalisation en Event-B
FIGURE 4.13 - Cas d'erreur
L'annexe B présente le reste des contraintes « OCL
».
|