De nos jours, les entreprises sont de plus en plus étendues et faisant collaborer plusieurs organisations pour la réalisation composée d'un objectif global. Des phénomènes tels que le commerce électronique et l'Internet stimulent en effet la coopération entre les organisations, donnant lieu a des processus métier inter-entreprises. Dans cette thèse de doctorat, nous proposons une approche ascendante pour vérifier l’interaction correcte entre des processus répartis sur un certain nombre d'organisations. Le modèle du système global étant indisponible, une approche d'analyse descendante est tout simplement impossible. Nous considérons deux critères de correction des processus métier inter-entreprises composés de deux (ou plusieurs) processus métier qui communiquent de manière synchrone et/ou asynchrone et/ou partageant des ressources. Le premier critère est générique et est exprimé par la propriété de soundness (robustesse), et certaines de ses variantes. Le deuxième critère est spécifique et peut être exprimé avec n'importe quelle formule de la logique temporelle linéaire. Chaque composante du processus global rend publique un modèle abstrait, représenté par un graphe appelé Graphe d'Observation Symbolique (GOS), permettant à la fois de préserver la confidentialité du processus local, la vérification de sa correction et de celle du processus global par composition de GOSs. Nous avons revisité et adapté le GOS afin de réduire la vérification du modèle composite à la vérification de la composition des abstractions des ses composants (leurs GOSs). Nous avons implémenté notre approche de vérification, basée sur le GOS, aussi bien pour les propriétés génériques que pour les propriétés spécifiques (LTL), et nous avons comparé les résultats obtenus avec ceux d'outils connus dans le domaine. Les résultats obtenus sont encourageants au vu du temps d’exécution et de l'espace mémoire consommés par notre technique. Ceci renforce notre conviction que le GOS est une structure appropriée pour l'abstraction et la vérification de processus métiers, en particulier lorsque ceux-ci sont faiblement couplés. / Today's corporations often must operate across organizational boundaries. Phenomena such as electronic commerce, extended enterprises, and the Internet stimulate cooperation between organizations. We propose a bottom-up approach to check the correct interaction between business processes distributed over a number of organizations. The whole system's model being unavailable, an up-down analysis approach is simply not feasible. We consider two correctness criteria of Inter-Enterprise Business Processes (IEBP) composed by two (or more) business processes communicating either synchronously or asynchronously and sharing resources : a generic one expressed with the well known soundness property (and some of its variants), and a specic one expressed with any linear time temporal logic formula. Each part of the whole organization exposes its abstract model, represented by a Symbolic Observation Graph (SOG), in order to allow the collaboration with possible partners. We revisited and adapted the SOG in order to reduce the verification of the entire composite model to the verification of the composition of the SOG-based abstractions. We implemented our verification algorithms, aiming at checking both specic and generic properties using SOGs, and compared our approach to some well known verification tools. The experimental results are encouraging in terms of both the construction time and the size of the abstraction's size. This strengthen our belief that the SOGs are suitable to abstract and to compose business processes especially when these are loosely coupled.