The BVM is a virtual machine that allows for the execution of B models by using the Brama tool’s animation core (Brama is a graphic animation tool).
Like the JVM (Java Virtual Machine), the BVM interprets B models and executes them in the execution environment provided by Brama. The use of the BVM therefore substitutes the classic chain of B software: refinement, translation, compilation and execution. Abstract B models can now be written and executed like computer programs. The BVM offers interfaces to initialize the programs’ data and provide outputs. These interfaces are written in Java. It also makes available means to load XML data to valuate the model’s abstract variables.
The program executed by the BVM may contain set-theoretic data and indeterministic substitutions. The program’s properties can be verified statically with Atelier B or dynamically by the BVM when executing the program events. This new way of programming with B allows for new possibilities and can be used, for example, to rapidly prototype software by using all the wealth of B Language or, another example, to insert within a Java application a module for which you want to prove the properties and that would be developed with B Method.