Débogage de modèles B événementiels en utilisant le plugin ProB disprover

Résumé

Le B classique, comme son sucesseur le B événementiel, sont toutes les deux des méthodes formelles utilisées pour le développement de systèmes informatiques dans lesquels l’exactitude est prouvée formellement. Cependant, plus la spécification devient complexe, plus des obligations de preuve doivent être déchargées. Bien que beaucoup de ces obligations de preuve peuvent être déchargées automatiquement par des outils tels que la plateforme RODIN, il en reste tout de même un nombre considérable à prouver interactivement. Cela peut être du à une preuve requise trop compliquée, ou à un modèle B erroné. Dans ce mémoire, nous décrivons un plugin disprover pour RODIN qui utilise l’animateur et model checker ProB pour trouver automatiquement des contre-exemples à une obligation de preuve problématique. Dans le cas où le disprover trouve un contre-exemple, l’utilisateur peut directement examiner la source du problème (comme mentionnée par le contre-exemple) et ne doit pas essayer de prouver l’obligation de preuve. Nous discutons également sous quelles conditions notre plugin peut être utilisé comme prover, c’est-à-dire quand l’absence de contre-exemples est en fait une preuve de l’obligation de preuve.

la date de réponse	2007
langue originale	Français
L'institution diplômante	Universite de Namur
Superviseur	Wim Vanhoof (Promoteur)