Aujourd'hui les outils IDM ont atteint un bon niveau de maturité et sont de plus en plus adoptés dans le cadre d'applications complexes et critiques. Toutefois, des questions liées à la sûreté des systèmes qui en découlent restent encore ouvertes. Pour répondre à ces questions, nous proposons de ramener l'IDM dans le monde rigoureux des méthodes formelles. Nos principaux objectifs sont : (1) garantir la cohérence des correspondances entre méta-modèles au moyen d'un outil de preuve, en l'occurrence le prouveur de l'atelier B ; (2) être capable de certifier qu'une transformation de modèles préserve la sémantique des modèles source et cible ; et (3) utiliser des outils d'animation de spécifications pour simuler le comportement des différents modèles mis en jeu dans un cadre IDM.