EVT2B – Traducteur B Evénementiel vers B

Développé par ClearSy dans le cadre du projet Européen MATISSE, cet outil permet de convertir des modèles B évènementiels vers des modèles B utilisables par l’Atelier B. EVT2B est en version beta, il est utilisé dans le cadre d’un certain nombre de projets industriels.

Pré-Requis

  • Système d’exploitation : Windows, Linux
  • Atelier B 3.7

Téléchargement

Archives

Documents

  • Manuel de référence du langage (pdf)
  • Manuel utilisateur (non maintenu depuis la version 3.6 de l’Atelier B) (pdf)

Utilisation

L’exécution d’EVT2B nécessite l’utilisation du « logic solver » krt (intégré à l’AtelierB), du fichier evt2b.kin (fichier compilé du langage de théorie) et d’un modèle B événementiel (fichiers .sys).

Assurez vous de renommer le fichier evt2b.kin.<plateforme>.<version_de_l’AtelierB> en evt2b.kin.

Placez-vous dans le répertoire contenant votre modèle B événementiel (fichiers .sys).

Pour chaque colonne de raffinement, vous devez créer un fichier de configuration contenant le texte suivant :

  • LoadComponent(<Machine>) & Analysis & WriteComponents où <Machine> est le nom de la machine la plus détaillée de la colonne.

Il vous reste à exécuter pour chaque fichier de configuration la commande suivante :

    • Sous Linux :  krt -p rmcomm -b evt2b.kin <fichier_de_configuration>
    • Sous Windows : krt.exe -p rmcomm -b evt2b.kin <fichier_de_configuration>

où <fichier_de_configuration> est le nom du fichier de configuration à traiter.

 

EVT2B va générer le modèle B équivalent : un fichier .mch et plusieurs fichiers .ref par colonne de raffinement.

Contact

Les commentaires sont fermés.