4.3 Formalisation en Event-B
Formaliser en Event-B consiste essentiellement à la
génération des deux composants Event- B : CONTEXT et MACHINE. Le
CONTEXT Event-B contient éventuellement la description statique du
modèle (déclaration des types, des constantes, etc) alors que la
MACHINE Event- B se focalise sur les aspects dynamiques du modèle
(déclaration des variables, des invariants, des
évènements, etc). Le processus de formalisation est abordé
en se basant sur le méta-modèle ECore contenant les concepts
structurels et comportementaux.
4.3.1 Formalisation du concept EPackage en Event-B
Dans le méta-modèle ECore, un package est
représenté par le méta-classe racine <EPa-ckage>. En
Event-B, un package sera représenté par CONTEXT, et aussi par
MACHINE (voir Figure 4.14).
FIGURE 4.14 - Formalisation du concept EPackage
page 64
4.3 Formalisation en Event-B
4.3.2 Formalisation du concept EClass en Event-B
En ECore, un class est représenté par la
méta-classe <EClass>. En Event-B, un class sera
représenté, dans le CONTEXT par l'ensemble EClassSet, et dans la
MACHINE par la variable EClassVariable. Pour chaque variable nous avons
associé un invariant de typage. Tel est l'invariant inv1 dans la Figure
4.15, et cette variable doit être initialisée dans Event
INITIALISATION.
FIGURE 4.15 - Formalisation du concept Eclass
4.3.3 Formalisation du concept EEnum en Event-B
Dans le méta-modèle ECore, les types
énumérés sont représentés par le concept
<EE-num>. En Event-B, Les types énumérés seront
traduits par des ensembles énumérés EEnum-Set dans la
clause SETS et tous ces EEnumLiteral sont formalisés en des
constantes(EEnumLiteral) dans CONTEXT Event-B. Pour chaque constant nous avons
associé un Axioms de typage. Tel est l'axioms axm1 dans la Figure
4.16.
4.3 Formalisation en Event-B
FIGURE 4.16 - Formalisation du concept EEnum
4.3.4 Formalisation du concept EAttribute en Event-B
Dans le méta-modèle ECore, un attribut d'EClass
est représenté par le concept <EAt-tribute>. En Event-B,
EAttribute sera représenté directement dans la MACHINE par la
variable « EAttributeVariable ». La fonction associée à
cette variable est donnée par l'invariant (inv2, inv3, inv4, inv5) qui
est une relation entre un EClass et le type de l'attribut « EDataType
». Pour chaque variable nous avons associé un invariant de typage,
et cette variable doit être initialisée dans Event
INITIALISATION.
La formalisation des attributs se fait naturellement à
l'aide des relations' entre les classes `EClass' et les types des
attributs'EDataType'. Cette approche est similaire à celle de [21]
[22].
Les spécialisations de la relation dépendent de
la nature de l'attribut : Selon que l'attribut est volatile ou non volatile,
unique ou non unique, la relation peut devenir une fonction partielle ou
totale. Le Tableau 4.1 donne les différentes valeurs de relation.
page 65
page 66
4.3 Formalisation en Event-B
TABLE 4.1 - prédicats avant-après
FIGURE 4.17 - Formalisation du concept EAttribute
La formalisation du concept "EAttribute" est donné par la
Figure 4.17.
page 67
4.3 Formalisation en Event-B
TABLE 4.2 - diverses relations fonctionnelles
en Event-B
| 
