Table des matières
Introduction générale 2
I Etat de l'art 5
1 Ingénierie dirigée par les modèles
6
1.1 Introduction 7
1.2 L'Ingénierie dirigée par les
modèles(IDM) 7
1.2.1 Principe et concepts généraux de l'IDM 7
1.2.2 L 'Approche MDA (Model Driven Architecture) 8
1.3 Transformation de modèles 10
1.3.1 Principe géneral d'une transformation 10
1.3.2 Types de transformation 11
1.3.3 Taxonomies des transformations 12
1.3.4 Paradigmes de transformation 12
1.3.4.1 Transformation Modèle vers Modèle 13
1.3.4.2 Transformation Modèle vers Code 14
1.4 Langage de transformation de modèles ATL 14
1.4.1 Vue d'ensemble sur la transformation ATL 15
1.4.2 Présentation d'ATL 16
1.5 La plateforme de modélisation sous Eclipse 18
1.5.1 Eclipse Modeling Framework (EMF) 18
1.5.2 XML Metadata Interchange (XMI) 19
1.6 Le langage de génération de code Xpand 20
1.6.1 Structure générale d'un template Xpand
20
1.7 Le langage Check pour la vérification de contraintes
21
page ii
TABLE DES MATIÈRES
|
2
|
1.8 MWE (Modeling Workflow Engine)
1.9 Conclusion
Méta-modélisation :Le
méta-modèle ECore
|
22
23
24
|
|
2.1
|
Introduction
|
25
|
|
2.2
|
La méta-modélisation
|
25
|
|
2.3
|
Les langages de méta-modélisation
|
26
|
|
|
2.3.1 MOF (Meta Object Facility)
|
26
|
|
|
2.3.2 ECore
|
26
|
|
2.4
|
Le Méta-modèle ECore
|
27
|
|
|
2.4.1 Noyau d'ECore
|
27
|
|
|
2.4.2 Caractéristiques structurelles
|
28
|
|
|
2.4.2.1 EAttribute
|
30
|
|
|
2.4.2.2 ERéférence
|
30
|
|
|
2.4.3 Caractéristiques comportementales
|
31
|
|
|
2.4.4 Classificateurs
|
33
|
|
|
2.4.4.1 Les classes
|
33
|
|
|
2.4.4.2 Types de données
|
34
|
|
|
2.4.4.3 Types énumérés
|
35
|
|
|
2.4.4.4 Package
|
36
|
|
2.5
|
Etude de cas
|
36
|
|
|
2.5.1 Présentation informelle
|
37
|
|
|
2.5.2 Spécification du système bancaire en ECore
|
37
|
|
2.6
|
Conclusion
|
38
|
|
3
|
La méthode formelle Event-B
|
39
|
|
3.1
|
Introduction
|
40
|
|
3.2
|
Quelques langages formels
|
40
|
|
|
3.2.1 Le langage Z
|
40
|
|
|
3.2.2 La méthode B
|
41
|
|
|
3.2.3 La méthode Event-B
|
41
|
|
3.3
|
Modèle Event-B
|
42
|
|
|
3.3.1 Structure d'une Machine
|
42
|
page iii
TABLE DES MATIÈRES
3.3.2 Structure d'un Contexte 43
3.3.3 Structure d'un Evénement 43
3.3.3.1 Les différentes formes des
événements 44
3.3.3.2 Obligations de preuves 46
3.4 Exemple de machine en Event-B 47
3.5 RODIN : l'outil support d'Event-B 48
3.6 Conclusion 49
II Contribution 50
4 Une approche IDM pour la génération de
modèle Event-B à partir de
modèle ECore 51
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.1.1 Méta-Classe de Context 52
4.2.1.2 Méta-Classe Machine 53
4.2.1.3 Méta-Classe Event 55
4.2.1.4 Vue d'ensemble sur le méta-modèle Event-B
55
4.2.1.5 Les règles de cohérences sous forme d'OCL
(.chk) 57
4.2.2 Méta-modèle ECore 59
4.2.2.1 Les règles de cohérence du
méta-modèle ECore sous forme
d'OCL (OCLinECore) 62
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
page iv
TABLE DES MATIÈRES
4.4.1.1 Exemple des règles en ATL 73
Règle générant Context et Machine
74
Règle générant les ensembles
abstraits(Sets) 75
Règle générant les
événements (Event) 76
Règle générant les Constants
(Constants) 77
Règle générant les ensembles
(Sets) 78
4.4.1.2 Exécution du programme ECore2Event-B.atl 79
4.4.2 Transformation de modèle M2T 81
4.4.2.1 Présentation de la transformation M2T 81
4.4.2.2 Modèle Event-B en texte: Extraction via Xpand
82
4.4.2.3 Le moteur de validation et de génération de
code Ada . . 84
4.4.2.4 Exemple d'utilisation : Système bancaire(Bank)
85
4.5 Vérification formelle par l'outil Rodin 88
4.5.1 Preuves d'une machine 88
4.6 Conclusion 91
Conclusion et perspectives 92
Appendices 94
Annexes 95
A Les règles de cohérence du
métamodèle Event-B sous forme d'OCL (.chk) 95
B Les règles de cohérence du
métamodèle ECore sous forme d'OCLinECore 98
C Les règles de transformation M2M
(Ecore2EventB.atl) 101
D Le template de génération de code EventB
en Xpand 110
v
| 
