NEPTUNE II Une plate-forme pour la vérification et la transformation de modèles

Leur utilisation grandissante lors des phases de specification et de conception confere aux modeles le rang de citoyen de premiere classe. Jusqu'ici utilises pour apprehender les logiciels a realiser, ils se voient attribuer un statut productif, central au developpement. Dans ce contexte, chaque activite d'un processus peut alors etre vue comme une transformation de modeles, automatisable ou partiellement automatisable. Ce nouveau statut des modeles et des meta-modeles pose le probleme de leur realisation et surtout de leur validation. Complementaire aux verifications realisees sur le code source, il est devenu necessaire de controler la qualite des modeles produits. Le controle de la transformation consiste a s'assurer que les modeles sources et cibles respectent un ensemble de proprietes verifiables, au travers de contrats de transformation. La plate-forme NEPTUNE II s'inscrit dans cette logique en permettant la verification de modeles et de leurs transformations, ce qui necessite en particulier la correction du typage d'expressions OCL navigant au travers de plusieurs meta-modeles.