site perso d’Emmanuel Dieul contact
plan du site
Photos
Expériences professionnelles
Logiciels
CV et références

VICS : vérification de raffinement B

samedi 7 novembre 2009

Contexte

VICS, Verification of an Implementation Conforming to its Specification, est un sujet de stage qui a été donné à Laïka Moussa lors de son stage de fin d’études (DESS DLS).

Sur un idée de Pierre-Yves Schobbens (professeur à l’Institut d’Informatique de Namur, FUNDP), j’ai encadré Laïka pendant son stage.

Sujet

Le développement formel via la méthode B se déroule en deux étapes :

  • l’écriture de spécifications
  • l’écriture de code implémentant ces spécifications Une étape de preuve vient ensuite assurer que le code écrit respecte bien les spécifications.

Lors de la preuve, certaines propriétés peuvent être très complexes à prouver : il est alors difficile de savoir si le code ne respecte pas la spécification. L’idée de VICS est de vérifier, via un moteur de résolution de contraintes, que le raffinement est correct.

JPEG - 73.9 ko
illustration d’une erreur d’implémentation

Rapport de stage et code source

Le développement de l’outil a été réalisé en Mozart/Oz car la machine virtuelle de ce langage interprété embarque un moteur de résolution de contraintes.

Le rapport de stage a posé les principes de la génération des contraintes et l’outil les a implémenté. Ce rapport est présenté ci-après et le code source est accessible sur le site de VICS.

PDF - 807.8 ko
rapport de stage de Laïka Moussa