Le contexte de cette thèse est la validation d'applications temps réel complexes, c'est- à-dire d'applications dont on doit garantir des propriétés temporelles d'ordre déterministe, et qui sont caractérisées par leur répartition et un développement relevant d'une conception multi-partenaires. Dans ce cadre, nous proposons des méthodes et des outils permettant cette validation à la fois par des approches d'analyse a priori et par des techniques formelles de tests de conformité. Une des idées de base du travail est d'utiliser le même formalisme, "Timed Input Output State Machine" (TIOSM), pour l'une et l'autre approches. Les travaux réalisés se sont traduits par plusieurs résultats. Dans les phases de validation a priori nous avons mis en ?uvre une technique énumérative de construction du graphe d'accessibilité d'un système composé de plusieurs TIOSMs communiquant et un algorithme de vérification de propriétés temporelles "à la volée". Dans la phase de test, nous avons développé une méthode de génération formelle de séquences de tests temporisés, dite adaptative, dont la caractéristique est de réduire le nombre de verdicts inconclusifs. De plus, nous avons proposé une méthode de validation hybride de systèmes complexes, par application conjointe d'analyse exhaustive de parties critiques et de simulation de l'ensemble du système. Enfin, nous avons proposé des traductions de modèles (entre TIOSM et réseaux de Petri temporels et de TIOSM vers SDL).