Institut National des Sciences Appliquéees de Lyon CITI Laboratory Université de Lyon

GénéSyst : Construction des comportements d'un modèle B

Contrat de diffusion des productions de l'équipe

Les différentes productions de l'équipe (BoB et GénéSyst en particulier) sont diffusées sous le contrat de licence CeCILL (Ce:CEA ; C:Cnrs ; I:INRIA ; LL:Logiciel Libre). Ces logiciels sont donc libres de diffusion et leur code source est accessible à tous (sur demande par mail). Cependant, il est impératif que tout utilisateur accepte les termes de la licence CeCILL (Version 2). Cette licence a été rédigée en 2 langues :

La BoB

La BoB (Boîte à Outils B) est un ensemble de classes Java permettant de manipuler des constructions B, telles que des substitutions ou des prédicats, et de notamment de calculer des prédicats de WP (Plus faible précondition). La mise en mémoire des machines et raffinement est effectuée par l'outil jbtools développé au LIFC.

Cette distribution est diffusée avec la librairie jbtools.

GénéSyst

GénéSyst est un ensemble de classes utilisant la BoB pour générer des systèmes de transitions étiquetées représentant le comportement exacte d'une spécification ou d'un raffinement B événementiel.

Pour plus d'information, se référer à :

  1. N. Stouls et M-L. Potet 2004. Explicitation du contròle de développement B événementiel(.ps.gz, .pdf), AFADL-04
  2. X. Morselli, M.-L. Potet et N. Stouls 2004. GénéSyst : Génération d'un système de transitions étiquetées à partir d'une spécification B événementiel(.ps.gz, .pdf), AFADL-04, Session outils. Article non soumis à concours.

Retour au plan