Depuis le milieu des années 1990, de nombreux modèles à composant ont vu le jour, comme Fractal développé par France Télécom et l'INRIA, OSGi développé par IBM, Click par le MIT, etc. Ces différents modèles ont tous pour but de pouvoir construire des programmes très larges et complexes, comme Eclipse basé sur OSGi ou la chaîne de compilation Fractal. Bien que ces modèles facilitent la conception de gros programmes, il est néanmoins toujours aisé de commettre des erreurs pouvant causer la levée d'une exception ou l'arrêt brutale du programme. Dans ce travail de thèse, nous nous intéressons à deux aspects de la validation des modèles à composant : nous définissons tout d'abord deux systèmes de types permettant de s'assurer qu'aucune erreur grave n'est présente dans un assemblage statique et typé ; nous étudions dans un simple langage de programmation Oz/K comment il est possible de décrire formellement l'interaction entre les composants et du code fonctionnel. Ce dernier langage nous a aussi permis d'étudier certaines commandes de manipulation d'assemblages qui seraient plus adaptées pour prouver des propriétés sur les programmes à base de composants.