Developed by ClearSy in the context of the European MATISSE project, this tool lets you convert Event B models into B models that can be used with Atelier B.  EVT2B is in Beta version and is used in the context of a number of industrial projects.

Prerequisites

  • Operating system: Windows, Linux
  • Atelier B 3.7

Download

Archives

Documents

  • Language reference manual (pdf)
  • User manual (not updated since version 3.6 of Atelier B) (pdf)

Use

EVT2B execution requires the use of the “logic solver” krt (integrated into Atelier B), the evt2b.kin file (compiled file of the theory language) and a B event model (.sys files).

Make sure you rename the evt2b.kin.<plateforme>.<version_de_l’AtelierB> file with evt2b.kin.

Go to the directory that has your B event model (.sys files).

For each refinement column, you need to create a configuration file that includes the following text:

  • LoadComponent(<Machine>) & Analysis & WriteComponents where <Machine> is the name of the machine in the column that has the most details.

Now, simply execute the following command for each configuration file:

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

where <fichier_de_configuration> is the name of the configuration file to be processed.

EVT2B will generate the equivalent B model: a .mch file and a number of .ref files per refinement column.

Contact