Sujet : Extension 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
L'outil GénéSyst est actuellement limité par le fait que les preuves permettant de calculer les transitions ne peuvent être faites que de manière automatique. Cependant, l'outil utilisé pour réaliser ces preuves permet également de les réaliser de manière interactive.
Le travail attendu dans ce stage est tout d'abord de réaliser un outil venant se greffer sur GénéSyst et fournissant un interface utilisateur utilisable permettant de choisir une obligation de preuve à simplifier ou d'intégrer dans le graphique produit une nouvelle simplification.
 
Dans le cas où le travail serait fait plus rapidement que prévu, de nombreuses extensions sont encore à faire autour de GénéSyst ...  
 
[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