4.3.5 Formalisation du concept EReference en Event-B
Une reference liant deux classes EClassA et EClassB (seront
représenté dans le CONTEXT par l'ensemble EClassASewt et
EClassBSet), est représentée dans le méta-modèle
ECore par la méta-classe <EReference>. En Event-B, une reference
sera traduite par une variable « EReferenceVariable » dans la clause
VARIABLES, typée ainsi au niveau de l'invariant de typage et
initialisé dans l'Event INITIALISATION. La variable EReferenceVariable
est une fonction entre EClassASet et EClassBSet.
Les spécialisations de la fonction dépendent des
multiplicités de « EReference » et leur EReference
opposé (UpperBound et LowerBound). Par exemple, des multiplicités
0 et 1 respectivement du coté de EClasssA et de EClassB, donnent lieu
à une fonction injection partielle de `EClassASet `vers `EClassBSet'. La
Figure 4.18 liste les diverses relations fonctionnelles en Event-B en leur
associant des multiplicités ECore.
4.3 Formalisation en Event-B
FIGURE 4.18 - Formalisation du concept
EAttribute
page 68
page 69
4.3 Formalisation en Event-B
4.3.6 Formalisation du concept EOperation en Event-B
En ECore, une opération est définit par le
méta-classe « EOperation » qui désigne les
opérations d'une classe, identifiée par un nom et des
paramètres « EParameter ». En Event-B, une opération se
traduit par un événement « EVENT », et ces
paramètres « EParameter » se traduit par PARAMETER.
Pour chaque paramètre<PARAMETER> d'un
événement<EVENT> nous avons associé un grade de
typage.
Example :
EOperationname(parameter1 : type, , .. .
, parametern : type).
FIGURE 4.19 - Formalisation du concept
EOperation
La formalisation de concept EOperation « est donné
par la Figure 4.19.
page 70
4.4 Transformations de modèle ECore vers Event-B en
utilisant une approche IDM (Ingénierie Dirigée par les
Modèles).
|