4.4.2.4 Exemple d'utilisation: Système
bancaire(Bank)
En exécutant le workflow sur le modèle Event-B
« Bank » présenté dans la partie
précédente (modèle cible de la transformation de
modèle ECore vers Event-B), nous obtenons les deux fichiers
générés « Bank.buc » et« Bank.bum
».
4.4 Transformations de modèle ECore vers Event-B en
utilisant une approche IDM (Ingénierie Dirigée par les
Modèles).
FIGURE 4.31 - Schéma de transformation
de modèle Event-B vers texte Event-B
Le fichier avec l'extension .buc représente le fichier
contexte dans un projet RODIN, Le contenu du ce fichier « Bank.buc
»est le suivant :(après une intervention manuelle).
page 86
page 87
4.4 Transformations de modèle ECore vers Event-B en
utilisant une approche IDM (Ingénierie Dirigée par les
Modèles).
Le fichier avec l'extension .bum représente une machine
dans un projet RODIN, Le contenu du ce fichier « Bank.bum » est le
suivant :(après une intervention manuelle)
page 88
4.5 Vérification formelle par l'outil Rodin
| 
