L'intelligence ambiante est considérée comme l'une des évolutions majeures de l'informatique ubiquitaire. Elle vise la mise en œuvre des environnements ambiants ou des espaces intelligents permettant d'améliorer la vie quotidienne des utilisateurs, leur bien-être et leur sécurité. Un environnement ambiant dispose d'une multitude d'équipements (capteurs, actionneurs), fournissant des services ubiquitaires atomiques qui sont distribués et de nature hétérogène. Ces services atomiques disponibles dans ce type d'environnement, ne répondent pas directement ou complètement à toutes les exigences et les besoins des utilisateurs. Par ailleurs, ces services de haut niveau peuvent impliquer l'interaction de services ubiquitaires appartenant et/ou contrôlés par différentes structures ou domaines (i.e. environnement multi-domaine). Dans ces travaux de thèse, on a étudié les problématiques reliées à l'agrégation des services ubiquitaires atomiques dans des coopérations et des compositions dans un environnement ambiant multi-domaine afin de répondre à des besoins utilisateurs. Cette étude concerne l'interopérabilité sémantique et comportementale des compositions de services ainsi que leurs spécifications dans un modèle formel basé sur la logique constructive BCDL0. Cette thèse a contribuée par la réalisation d'un canevas sémantique permettant la conception et la vérification formelles des processus coopératifs dans l'assistant à la preuve Isabelle/HOL. Le canevas sémantique proposé consiste en une ontologie de coopération extensible et un langage de spécification de services fiable (Sound) ainsi que des modules de mise en correspondance vers des infrastructures cibles / Ambient Intelligence is considered as the major application domain of ubiquitous computing. It aims at implementing intelligent environments to improve the daily activities, the well-being and the safety of users. An ambient environment has a multitude of devices (sensors, actuators), providing atomic ubiquitous services which are distributed and heterogeneous. These atomic services available in these environments, do not directly or fully meet all the requirements and the needs of users. Moreover, these high-level services may involve the interaction of ubiquitous services owned and/or controlled by different structures or domains (i.e. multi-domain environment). In this work, we studied the problems related to the aggregation of atomic ubiquitous services in cooperations and compositions in an ambient multi-domain environment in order to meet users' needs. This study concerns the semantic and behavioral interoperability of high-level composite services and their formal specification. This latter, is based on the Basic Constructive Description Logic, namely, BCDL0 formal model. This work contributes by realizing a semantic framework for the design and formal verification of cooperative processes in the interactive theorem prover Isabelle/HOL. The proposed semantic framework consists of an extensible cooperation ontology, a sound formal specification language of ubiquitous services and a components for mapping the formally proved cooperatives processes to the targeted infrastructures