Une approche IDM du transformation du modèle ecore vers event-b.

4.2.1.2 Méta-Classe Machine

Comme indiqué dans le chapitre 3, une machine est constituée de plusieurs clauses permettant de spécifier les parties statiques et dynamiques du système. La partie statique

4.2 Les méta-modèles de notre approche

correspond aux déclarations de variables et une caractérisation de ces données en termes d'invariants. Quant à la partie dynamique, elle est spécifiée par EVENT et INTIALISA-TION qui permettent de représenter respectivement les événements et l'initialisation d'une spécification Event-B. La description de la machine est constituée d'un ensemble de clauses et est montré par la Figure 4.3 suivante :

MACHINE Machine_identifier SEES * context_identifier_list VARIABLES Variable_identifier_list INVARIANTS label: <predicate> EVENTS <event_list> INTIALISATION

END

FIGURE 4.3 - Structure d'une machine

De cette description nous pouvons dériver le méta-modèle d'une machine comme il est montré par la Figure 4.4 :

page 54

FIGURE 4.4 - Méta-Classe Machine

Les méta-classes `Event','Variable, `Variant','Invariant' sont incluses dans la méta-classe `Machine' qui définit la partie dynamique du modèle Event-B.

page 55

4.2 Les méta-modèles de notre approche

4.2.1.3 Méta-Classe Event

La méta-classe `Event' est une sous classe de 'Machine'. Celle-ci est composée de quatre sous méta-classes `Parameter' , `Guard' , `Action' , `Witness' présentées par la Figure 4.5.

FIGURE 4.5 - Méta-Classe Event

4.2.1.4 Vue d'ensemble sur le méta-modèle Event-B

Le méta-modèle Event-B utilisé comme méta-modèle cible pour notre approche de transformation de ECore vers Event-B est l'assemblage de toutes les méta-classes (Context, Machine, Event) déjà présentées dans cette section. Les Figures 4.6 et 4.7 illustrent ce méta-modèle.

variables

4.2 Les méta-modèles de notre approche

Vatiable

C...

name : EString

irr ariantt

p Invariant

	4 name : EStrittg § refinesName : ratting § seesNarne : EShing
refines

0..¹ mine ; EStnog

preckat:ESbi

o,.

			Variant
	variants		T maw:^. E5trrng § pretCcat : E51rin9	§	§
			Event

refines

0.' $ name : EStriurg

$ extended : Boolean

§ retinesNwme ; ES#r.rg

senumeralionJ coriverse_

- Y

- .tamergent

- anticipated

SeS

sees

o,.

extends

o,.

A Sets

_Q-.

name : E51nng

Context

§ 4Sar1é; ESteinsj

? extendedName ; EStr.'ig

- Constant

$

€ons[ants name : Mring

o..

fl Axiam $ name : EString predieat _ EStrin9

ao iorns

o.,

FIGURE 4.6 -- Méta-modèle Event-B

page 56

page 57

4.2 Les méta-modèles de notre approche

FIGURE 4.7 - Méta-modèle Event-B ouvert avec son éditeur