Sujet : Intégration de Barvey à GénéSyst
 
Publique visé : Magistère 1 et 2.
 
Laboratoire : LSR-IMAG, Campus.
 
Responsables : Didier Bert & Nicolas Stouls.
 
Cadre du travail
Initiallement, la méthode formelle B a été conçue et utilisée comme une méthode de développement de logiciels dans lesquels on s'intéresse aux données et aux traitements. L'introduction des événements, et la notion associée de raffinement, permet la prise en compte des aspects comportementaux des systèmes. Le raffinement devient alors un outil très puissant qui permet de décrire les systèmes suivant différents degrés de granularité. Les modèles sont alors plus complets et les processus de spécification et de raffinement deviennent, quant à eux, plus complexes. Il devient nécessaire d'offrir des outils de plus haut niveau permettant d'assister à la fois la spécification et la preuve.
 
Nous avons réalisé un outil, GénéSyst, qui permet de visualiser le comportement de modèles B sous forme de systèmes de transitions symboliques. L'approche, intialement proposée dans [BC00], a été étendue dans [PS04] pour prendre en compte le raffinement. Les systèmes de transitions sont alors hiérarchisés. Nous explicitons la construction de ces systèmes de transitions et donnons des conditions qui permettent de construire des représentations ayant de bonnes propriétés, en terme de structuration.
 
Cette génération est réalisée par le biais d'obligations de preuves qui sont vérifiées. Actuellement cette verification est réalisée de manière automatique par un outil extérieur appelé Atelier B. Cependant, il semble pertinent de s'ouvrir à d'autres prouveurs tels que HarVey qui semblent plus puissants et rapides dans certains cas qu'il reste à définir.
 
Description du travail
Le travail attendu dans ce stage est avant tout la réalisation d'une interface qui permettra à GénéSyst d'utiliser le prouveur HarVey (au travers de l'outil Barvey qui permet de faire le lien avec la méthode B), mais aussi une étude théorique sur les limitations de ce nouveau prouveur et la réalisation de quelques cas d'études permettant d'exhiber les avantages de chacuns de prouveurs.
 
 
[BC00] : D. Bert et F. Cave, "Construction of Finite Labelled Transition Systems from B Abstract Systems", Springer-Verlag, LNCS vol.1945, 2000.
[PS04] : M-L Potet et N. Stouls, "Explicitation du contròle de développement B événementiel", AFADL 2004.
 

---

Nicolas Stouls, en thèse à l'INP Grenoble au laboratoire LSR Nicolas.Stouls@imag.fr Bur. D.320                             tel. 04.76.82.72.74 http://www-lsr.imag.fr/Les.Personnes/Nicolas.Stouls/

Didier Bert, chargé de recherche au LSR Didier.Bert@imag.fr Bur. D323                             tel. 04.76.82.72.16 http://www-lsr.imag.fr/Les.Personnes/Didier.Bert/

LSR-IMAG 681 rue de la Passerelle, BP. 72, 38402 St Martin d'Hères Cedex FRANCE