L'interopérabilité revêt un enjeu majeur pour l'industrie et son absence peut être vue comme un des principaux freins à un travail collaboratif, et plus particulièrement dans les processus collaboratifs aussi bien publics (inter-entreprises) que privé (intra-entreprise). Il parait donc pertinent d'analyser et de détecter d'éventuels manques ou défauts d'interopérabilité dans des entreprises impliquées dans un processus collaboratif. Les recherches en interopérabilité ont montré l'intérêt de mesurer et d'évaluer l'interopérabilité avec la proposition de cadres et de modèles de maturité dans le but d'éviter d'éventuels problèmes d'interopérabilité. Cependant, des approches de détection et d'anticipation de problèmes d'interopérabilité n'existent pas à notre connaissance. Les travaux de recherche proposés dans cette thèse se développent dans un contexte d'ingénierie de processus guidée par les modèles et se proposent d'utiliser des techniques de vérification formelle pour détecter différents types de problèmes ou de pré-somption de problèmes d'interopérabilité. Ceci implique, dans un premier temps, de définir les besoins particuliers en interopérabilité devant être pris en compte dans un contexte colla-boratif. Dans un second temps, il est nécessaire de formaliser ces besoins en un ensemble d'exigences d'interopérabilité, de manière aussi formelle que possible. Ceci a abouti à quatre classes d'exigences d'interopérabilité respectant le cycle de vie d'un processus collaboratif : les exigences de compatibilité, les exigences d'interopération, les exigences d'autonomie et les exigences de réversibilité. Enfin, ces exigences doivent être vérifiées en se référant aux modèles du ou des processus étudiés.