Outil d'aide à la localisation des erreurs dans les modèles PRISM
Loading...
Date
2016-06-10
Journal Title
Journal ISSN
Volume Title
Publisher
University of M'sila
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.
Description
Keywords
Vérification formelle , Le model checking probabiliste ,outil PRISM ,contre-exemple probabiliste , localisation d'erreurs .