Mise en œuvre d’une approche formelle en ingénierie des modèles

International audienceL’ingénierie des modèles (IDM) prone l’utilisation de modèles tout au long du cycle de développement de logiciels dans le but d’augmenter le niveau d’abstraction et réduire ainsi la complexité du logiciel. L’intérêt de cette ap- proche est qu’elle permet d’avoir une séparation claire des préoccupations allant de modèles d’exigences jusqu’à la mise en oeuvre dans des plateformes cibles, tout en passant par les divers modèles de conception. Cependant, une limitation majeure de l’IDM est le manque d’outils de raisonnement formel permettant de garantir la correction des modèles issus des différents niveaux d’abstraction. En effet, la plupart des activités de validation offertes par les outils IDM d’au- jourd’hui (en l’occurrence EMF, Eclipse Modeling Framework) sont basées sur la vérification de contraintes OCL à partir d’instances de méta-modèles sans pour autant garantir que ces instances se comportent conformément aux proprié- tés attendues. Dans ce travail, nous présentons un outil dédié à réduire le fossé entre l’IDM et le monde rigoureux des méthodes formelles. L’outil repose sur la traduction de méta-modèles EMF en une spécification B équivalente et permet l’injection de modèles dans cette même spécification. Cette technique vise à tirer pleinement profil d’outils de raisonnements formels tels que les outils de preuve et de model-checking. Il devient en effet possible de spécifier le comportement du modèle EMF en B ainsi que ses propriétés invariantes. L’AtelierB sera uti- lisé pour prouver la correction de ce comportement, et le model-checker ProB sera utilisé pour animer des scénarios d’exécution sous-jacents et les remonter au niveau du modèle EMF de départ