aLe caractère distribué des nouvelles architectures embarquées fait apparaître de nouveaux problèmes dans le développement des systèmes. En effet, leur comportement asynchrone nécessite la mise en œuvre de techniques permettant, d’une part, la prise en compte de ce phénomène au niveau de la spécification, et, d’autre part, d’aider à la validation de ces systèmes. C’est dans le cadre de la vérification formelle et, plus particulièrement, dans l'application du "model checking" que les travaux présentés dans ce mémoire s’inscrivent. Après une présentation des techniques couramment utilisées dans le domaine des systèmes temps-réel, la première partie de ce mémoire est consacrée à l’étude d’un modèle formel permettant la spécification des systèmes embarqués distribués. Ce modèle est fondé sur la définition d’une architecture fonctionnelle, d’une plateforme d’exécution et d’une fonction d’allocation. Afin de rendre possible la vérification formelle d’un système, deux étapes de transformation sont détaillées afin de mener à l'expression du modèle de spécification dans le formalisme des automates temporisés. En second lieu, nous présentons une méthode de vérification basée sur l'abstraction d’un système. Si l'abstraction d’un système tend à limiter l’espace des états d’un système, cette technique fait naître de nouvelles propriétés devant être vérifiées. Pour ce faire, nous proposons un cadre compositionnel permettant de dégager ces obligations de preuve. La validation d’une exigence conduit alors à valider les obligations de preuve engendrées par l'abstraction du modèle et l'exigence elle-même.