Warning: include(../../include/menu-fr.php) [function.include]: failed to open stream: No such file or directory in /homepages/5/d101319127/htdocs/atelierb.eu/ressources/evt2b/evt2b-fr.php on line 34

Warning: include() [function.include]: Failed opening '../../include/menu-fr.php' for inclusion (include_path='.:/usr/lib/php5') in /homepages/5/d101319127/htdocs/atelierb.eu/ressources/evt2b/evt2b-fr.php on line 34

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<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>
  • <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