Étude sur la modélisation et la vérification probabiliste d'architectures de simulations distribuées pour l'évaluation de performances

L'objectif dé ni dans cette thèse est d utiliser les récentes techniques de model checking probabiliste a n de véri er 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 a n de formuler et de véri er 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 dif cile de choisir les coef cients 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. A n 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 dif cilement compréhensibles et manipulables. A n 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 a n 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.TOULOUSE-ISAE (315552318) / SudocSudocFranceF