Une application temps réel est une application dont le comportement ne dépend pas seulement du résultat logique du calcul, mais aussi de la date à laquelle ce résultat est produit. Pour garantir la conformité de ce comportement par rapport aux spécifications de départ, on applique durant le cycle de vie d'une application temps réel des méthodes de validation de propriétés a priori et a posteriori. Dans ce document, nous introduisons la notion de propriétés temporelles complexes à vérifier sur de telles applications. Pour vérifier a priori ces types de propriétés, nous proposons des méthodes de décomposition de modèles. Cette décomposition sera exploitée par des méthodes de vérification afin d'optimiser les calculs et ainsi réduire la complexité. Nous nous appuyons sur les informations obtenues au cours du model-checking pour guider le concepteur dans le développement d'un système correct par une méthode d'aide à la correction du système et de son modèle en cas d'échec lors de la validation. Pour vérifier a posteriori de telles propriétés, nous proposons des méthodes de génération de testeurs temporisés permettant l ‘amélioration de la couverture de test. Dans ces méthodes , nous introduisons des heuristiques dans le testeur afin d'optimiser ses calculs. Notons enfin que nous avons choisi pour effectuer nos travaux le formalisme des TIOSMs qui est particulièrement adapté pour modéliser des applications temps réel communicantes. || A real time application is an application in which the behaviour doesn't only rely on the logic result but also on the date at which the result is obtained. In order to prove that the behaviour of an application is conform to its specification, we applied