Sujet : Vérification et optimisation de l'outil GénéSyst
 
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 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.
 
Description du travail
Le travail attendu dans ce stage est avant tout une vérification de la correction des formules implantées par rapport aux théories développées. Mais il sera aussi attendu un travail d'optimisation de  l'outil et, si possible, une étude sur les bonnes propriétés de l'atteignabilité et sur les gains possibles par rapport à l'outil en cas d'implantation.
 
 
[BC00] : D. Bert et F. Cave, "Construction of Finite Labelled Transition Systems from B Abstract Systems", Springer-Verlag, LNCS vol.1945, 2000.
 

---

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