L'objectif défini dans cette thèse est d’utiliser les récentes techniques de model checking probabiliste afin de vérifier des contraintes de performances sur des architectures de simulations distribuées. L'aspect probabiliste de l'approche permet à la fois de réduire la complexité du modèle et d’exprimer des contraintes de performances plus souples. Dans cette thèse nous avons dans un premier temps tenté d’utiliser le model checking probabiliste afin de formuler et de vérifier de telles contraintes de performances. Nous avons utilisé le model checker PRISM et confronté les résultats obtenus avec des données réelles provenant de simulations distribuées. Ceci a permis de révéler une difficulté fondamentale de cette démarche : il est difficile de choisir les coefficients du modèle pour que les résultats obtenus par le model checker coïncident avec la réalité. En clair, le modèle doit être réaliste. Afin de surmonter cette difficulté nous avons d’abord utilisé des algorithmes d'approximation qui ont permis d’obtenir des modèles plus réalistes mais sans structure, les rendant difficilement compréhensibles et manipulables. Afin de remédier à ce problème nous avons adapté un de ces algorithmes d’approximation, permettant d’induire des distributions de type phase à partir d’un ensemble de temps d’absorption, pour lui permettre d’opérer sur des modèles décrit dans l’algébre PEPA, un langage de modélisation basé sur une approche compositionnelle. L'algorithme a ensuite été étendu afin de fonctionner avec des exécutions partiellement observables au lieu de temps d’absorption, permettant ainsi de travailler sur des modèles PEPA sans état absorbant. Les expérimentations s’appuient sur le logiciel EMPEPA, distribué librement en Open-source, développé dans le cadre des travaux de thèse, et implantant en particulier ces deux algorithmes.