Sujet : Extension de MecV + IHM



Responsable : K. Musumbu
Téléphone : 05 40 00 38 76

e-mail : musumbu@labri.fr

Présentation du sujet : MecV est un outil du model-checking, qui utilse les marquages des états pour vérifier les propriétés desirées ou non souhaitées des systèmes concurrents. Le problème est que les systèmes concurrents sont construits par synchronisation des systèmes. Par contre, il y a une perte d'information concernant les proriétés élémentaires vérifiées par états. Il s'agira dans certain cas de regénérer (restituer) ces informations. Il s'agit donc d'enrigir MecV avec des nouvelles fonctionnalités dont les utilisateurs ont besoin. Si le temps le permet, proposer une interface graphique conviviale facilitant l'usage de l'outil.

Tavail à faire :
  1. Permettre dans la synchronisation l'expression de l'action ne rien faire
  2. Soit une propriété élémentaire partagée par tous les systèmes du produit symchronisé, interagir avec l'utilisateur pour confirmer ou infirmer si c'est syntaxique ou sémantique, dans le deuxième cas de figure, marquer les états correspondants du produit synchronisé.
  3. Une fonction qui renvoie l'indice du bit libre
  4. une fonction qui renvoie l'indice du bit qui code une propriété élémentaires donnée
  5. Permettre de marquer certains états avec des valeurs entières
  6. etc.


Mot-clés : Model-checking, système de transitions étiquées, synchronisation

Références : notes du cours,

Commentaires éventuels : Ce sujet est fortement recommandé aux étudiants qui ont suivi l'UE Technologie de la Vérification, qui constitue le pré-requis nécessaire.