Outil d'aide à la localisation des erreurs dans les modèles PRISM

Abstract

Dans ce mémoire, nous proposons un outil d'aide ä la localisation des erreurs qui apparaissent lors de la vérification de systemes probabilistes en utilisant la technique du model checking probabiliste avec l'outil PRISM. Le model checking probabiliste est une technique de vérification qui consiste ä déterminer si un modele probabiliste M vérifie une propriété donnée. Les modéles sont décrits par des systémes de transitions tandis que la logique temporelle est utilisée comme langage de spécification des propriété . Ce mémoire aborde pour la premiere fois une tåche du vérification totalement automatique des modéle PRISM , pour lequel un contreexemple est disponible . Nous présentons les résultats des premiéres exprérimentations qui sont encourageants.