4.6 Conclusion
D
ans ce chapitre, nous avons proposé un
méta-modèle Event-B ainsi qu'une transformation de modèle
ECore en modèle Event-B en respectant des contraintes exprimées
en OCLinECore et en utilisant ATL comme langage de transformation M2M. Nous
avons, par ailleurs, proposé une transformation de modèle Event-B
en texte en respectant des contraintes exprimées en Check et en
utilisant l'outil Xpand qui nous a permis de transformer un modèle
Event-B vers code moyennant l'écriture des templates Xpand. Nous avons
vérifié le modèle Event-B obtenu avec l'outil RODIN.
92
| 
