Deuxième partie
50
Contribution
51
4 Une approche IDM pour la généra-
tion de modèle Event-B à partir de
modèle ECore
Sommaire
4.1 Introduction 52
4.2 Les méta-modèles de notre approche
52
4.2.1 Méta-modèle Event-B 52
4.2.2 Méta-modèle ECore 59
4.3 Formalisation en Event-B 63
4.3.1 Formalisation du concept EPackage en Event-B 63
4.3.2 Formalisation du concept EClass en Event-B 64
4.3.3 Formalisation du concept EEnum en Event-B 64
4.3.4 Formalisation du concept EAttribute en Event-B 65
4.3.5 Formalisation du concept EReference en Event-B 67
4.3.6 Formalisation du concept EOperation en Event-B 69
4.4 Transformations de modèle ECore vers Event-B
en utilisant une approche IDM (Ingénierie Dirigée par les
Modèles). . . . 70
4.4.1 Transformation de modèles M2M 71
4.4.2 Transformation de modèle M2T 81
4.5 Vérification formelle par l'outil Rodin
88
4.5.1 Preuves d'une machine 88
4.6 Conclusion 91
page 52
4.1 Introduction
4.1 Introduction
C
e chapitre comporte quatre sections, la première
section présente les méta-modèles Event-B et ECore que
nous utilisons dans notre contexte de transformation. Dans la deuxième
section nous présentons notre contribution qui consiste à la
formalisation en Event-B des concepts ECore. Dans la troisième section
nous présentons la transformation des modèles M2M (ECore2Event-B)
en utilisant ATL comme langage de transformation, ensuite nous
présentons la transformation M2T (Event-B2TexteEvent-B).Et enfin nous
présentons la validation sur la plateforme RODIN.
4.2 Les méta-modèles de notre
approche
Pour définir un langage de modélisation, il est
nécessaire de définir sa syntaxe abstraite et sa syntaxe
concrète. Les méta-modèles représentent pour notre
approche la base de la transformation. Pour chacune de ces transformations,
chaque modèle est défini dans son propre
méta-modèle.
4.2.1 Méta-modèle Event-B
Le méta-modèle que nous proposons pour Event-B
donne une vue structurelle de haut niveau reprenant les notions définies
au niveau de la syntaxe Event-B. Nous nous en servons ici pour donner une
vision globale des dépendances entre les différentes
constructions du langage Event-B. Dans un premier temps, nous
procéderons à la spécification du fragment du
méta-modèle correspondant à une machine Event-B, ensuite
nous proposerons un fragment du méta-modèle exprimant le contexte
Event-B ainsi qu'un fragment du méta-modèle exprimant
l'événement. Et Enfin nous terminerons par une vue d'ensemble de
notre méta-modèle Event-B utilisé comme
méta-modèle cible pour notre approche de transformation ECore
vers Event-B.
4.2.1.1 Méta-Classe de Context
Un Context représenté est constitué de
plusieurs clauses permettant de spécifier les parties statiques du
système. La partie statique correspond aux déclarations
d'ensembles, de constantes et d'axiomes décrivant les
propriétés de ces constantes.
page 53
4.2 Les méta-modèles de notre approche
La description du contexte est constituée d'un ensemble de
clauses et est montrée par la Figure 4.1 suivant :
|
CONTEXT Context_ identifier_list SETS set_identifier 1
CONSTANTS constant_identifier1 AXIOMS * label_1 :
<predicate_1> END
|
FIGURE 4.1 - Structure d'un contexte
De cette description nous pouvons dériver le
méta-modèle d'un contexte montré dans la Figure 4.2 au
dessous :
FIGURE 4.2 - Méta-Classe Context
La Méta-Classe « Context » définit la
partie statique du modèle Event-B. Elle est composée de trois
sous Méta-Classe `Sets','Constants' et `Axioms'. Chacune d'entre elles
contient un Méta-Attribut `name' (de type chaine de
caractères).
| 
