Table des figures
1.1 les relations de bases dans IDM 8
1.2 Exemple montrant les relations de bases dans IDM 8
1.3 Pyramide de modélisation de l'OMG 10
1.4 Transformation de modèles 11
1.5 Approches de transformations de modèles 13
1.6 Vue d'ensemble sur la transformation ATL 15
1.7 Les règles de transformation ATL 17
1.8 Aperçu d'un fichier ECore ouvert avec son
éditeur 19
1.9 Exemple d'un fichier XMI 20
2.1 Notions de base de la méta-modélisation
25
2.2 Les concepts du méta-modèle ECore 27
2.3 Noyau d'ECore 28
2.4 Concept EStructuralFeature 29
2.5 Concept EAttribute 30
2.6 Concept EReference 31
2.7 Concept EOperation et EParameter 32
2.8 Concept EClassifier 33
2.9 Concept EClass 34
2.10 Concept EDataType, EEnum et EEnumLiteral 35
2.11 Concept EPackage 36
2.12 Modèle ECore d'un Bank 37
2.13 Modèle ECore d'un Bank validé 38
3.1 L'unité de spécification de Z 41
3.2 Relation entre un contexte et une machine 43
page vi
TABLE DES FIGURES
3.3 La plateforme RODIN 49
4.1 Structure d'un contexte 53
4.2 Méta-Classe Context 53
4.3 Structure d'une machine 54
4.4 Méta-Classe Machine 54
4.5 Méta-Classe Event 55
4.6 Méta-modèle Event-B 56
4.7 Méta-modèle Event-B ouvert avec son
éditeur 57
4.8 Cas d'erreur 58
4.9 Cas de warning 59
4.10 Méta-modèle ECore ouvert avec son
éditeur 60
4.11 Méta-modèle ECore partiel 61
4.12 Règle sous forme d'OCLinECore. 62
4.13 Cas d'erreur 63
4.14 Formalisation du concept EPackage 63
4.15 Formalisation du concept Eclass 64
4.16 Formalisation du concept EEnum 65
4.17 Formalisation du concept EAttribute 66
4.18 Formalisation du concept EAttribute 68
4.19 Formalisation du concept EOperation 69
4.20 Schéma de notre approche 70
4.21 Vue d'ensemble sur le programme ECore2Event-B 72
4.22 Exemple règle ATL 73
4.23 Règle générant Context et Machine
75
4.24 Règle générant Sets 76
4.25 Règle générant Event 77
4.26 Règle générant Constants 78
4.27 Règle générant Sets 79
4.28 Modèle ECore d'un Bank (modèle source)
80
4.29 Modèle Event-B d'un Bank (modèle cible)
80
4.30 Schéma de transformation de modèle Event-B
vers texte Event-B 81
4.31 Schéma de transformation de modèle Event-B
vers texte Event-B 86
page vii
TABLE DES FIGURES
4.32 Les OPs sous Rodin de la machine 89
4.33 Preuve automatique 90
4.34 Preuves interactif 91
1
Liste des tableaux
3.1 prédicats avant-après 46
4.1 prédicats avant-après 66
4.2 diverses relations fonctionnelles en Event-B 67
2
Introduction générale
L
es logiciels et systèmes informatiques sont
présents aujourd'hui dans tous les domaines
de l'activité humaine (industrie, construction,
communication...). Avec le temps ces
logiciels deviennent de plus en plus
complexes, et par conséquent, leur analyse et leur vérification
représentent un enjeu capital. Ceci les rend très sensibles aux
erreurs produites durant le cycle de vie d'un système. En effet, ces
erreurs logicielles peuvent être introduites durant la phase de
conception.
Pour la conception du logiciel, Les méthodes les plus
utilisées en conception de systèmes d'information (ECore, UML)
dites semi-formelles, sont basées principalement sur l'utilisation de
divers diagrammes. Ces méthodes présentent des avantages
indéniables. Elles représentent le système d'une
manière à la fois intuitive et synthétique. De ce fait,
elles sont bien adaptées à la plupart des utilisateurs. Ces
avantages ont contribué à répandre largement leur
utilisation dans l'industrie. Mais leur principal défaut est l'absence
d'une sémantique précise des diverses notations utilisées,
ce qui entraîne souvent des ambiguïtés. En outre, il est
impossible de prouver la cohérence du système, ce qui limite la
fiabilité des logiciels produits.
Pour réagir face à ces problèmes, il est
nécessaire d'offrir des méthodes permettant d'éviter les
erreurs inhérentes au développement des logiciels et
systèmes complexes. Le génie logiciel offre des méthodes,
techniques et outils permettant de vérifier et d'éviter les
erreurs. En effet, les méthodes formelles du génie logiciel
fournissent des notations issues des mathématiques, en particulier de la
logique, permettant de décrire très précisément les
propriétés des systèmes à construire. De ce fait,
ces méthodes disposent de techniques de preuve permettant de
vérifier complètement le raffinement des spécifications en
code exécutable. Ces avantages apportent des réponses pertinentes
à la problématique de construction des logiciels et
systèmes complexes.
page 3
Introduction générale
L'objectif de ce mémoire est de proposer une approche
IDM de la transformation Du méta-modèle ECore vers la
méthode formelle Event-B basée sur le principe « tout est
modèle » [6]. Pour y parvenir, nous avons élaboré
deux méta-modèles : le méta-modèle ECore jouant le
rôle de méta-modèle source et le méta-modèle
Event-B jouant le rôle de méta-modèle cible pour
l'opération de transformation d'ECore vers Event-B. De plus, nous avons
réalisé un programme ECore2Event-B écrit en ATL [8]
permettant de transformer un modèle source conforme au
méta-modèle ECore vers un modèle cible conforme au
méta-modèle Event-B. En outre nous avons utilisé avec
profit l'outil de Xpand pour la transformation du modèle Event-B
à un code Event-B. Enfin, nous avons testé notre travail sur une
étude de cas d'un Système Bancaire « BANK »
décrite en [3].
Ce mémoire contient deux grandes parties qui sont
organisées de la manière suivante :
~ Partie I : Etat de l'art
-- Le chapitre 1
premier chapitre donne une vue d'ensemble sur l'approche IDM.
En outre, il présente ATL comme un langage de transformation M2M, aussi
Xpand comme un langage de transformation M2T et enfin la plateforme Eclipse
utilisé dans ce mémoire.
-- Le chapitre 2
Le second présente la méta-modélisation
semi-formelle ECore et les concepts du méta-modèle ECore qui joue
le rôle de méta-modèle source de notre approche de
transformation.
-- Le chapitre 3
Le troisième chapitre présente d'une
façon rigoureuse les principes du langage Event-B (machine abstraite,
contexte, langage de substitutions, obligations de preuves) permettant de
développer des modèles corrects par construction. Il
présente aussi un aperçu sur la plateforme RODIN [27] [28]
supportant la méthode Event-B.
page 4
Introduction générale
~ Partie II : Contribution
-- Le chapitre 4
Le dernier chapitre est consacré au passage du
modèle ECore vers Event-B. Ce chapitre comporte quatre sections, la
première section présente les méta-modèles, Event-B
et ECore que nous les utilisons dans notre contexte de transformation. Dans la
deuxième section nous présentons notre contribution 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) et la transformation M2T
(Event-B2TexteEvent-B).Et enfin nous présentons la validation du
modèle cible Event-B sur la plateforme RODIN.
Enfin, nous achèverons notre mémoire par une
conclusion et des perspectives.
| 
