Les notations semi-formelles et formelles semblant complémentaires, leur couplage semble un cadre intéressant pour pouvoir bénéficier de leurs avantages respectifs tout en diminuant leurs points faibles. En effet, d'une part, les notations semi-formelles qui pêchent par leur précision sont de bons vecteurs de communication dont le coût de formation est raisonnable ; d'autre part, les langages formels apportent la précision et le potentiel de raisonnement manquant aux notations semi-formelles. Dans ce travail, nous proposons une approche de traduction de modèles semi-formels objet en des spécifications formelles en Z ou en Object-Z afin de fournir un couplage bénéfique de ces deux types de spécifications. Nous cherchons à rendre nos propositions les plus utilisables possible en en montrant trois bénéfices avérés : un guide méthodologique pour l'expression des contraintes annotant un modèle objet, une aide à la vérification des modèles et de leurs contraintes et des raisonnements informels sur la sémantique de modèles simples. Nous avons aussi développé un outil de support à notre approche, RoZ qui permet de faire cohabiter les notations semi-formelles et formelles. Enfin nous étudions une autre approche de couplage, la vérification de cohérence par méta-modélisation pour laquelle nous proposons des règles de cohérence entre le modèle objet et Z. Ce travail nous permet de comparer cette approche avec notre stratégie de traduction afin de mieux comprendre leurs avantages et leurs inconvénients.