La BVM est une machine virtuelle permettant d’exécuter des modèles B en utilisant le cœur d’animation de l’outil Brama, un outil d’animation graphique.

Au même titre que la JVM (Java Virtual Machine), la BVM interprète les modèles B et les exécute dans l’environnement d’exécution fourni par Brama. Ainsi l’utilisation de la BVM se substitue à la chaîne classique du B logiciel : raffinement, traduction, compilation, exécution. Il devient ainsi possible d’écrire des modèles B abstraits et de les exécuter comme des programmes informatiques. La BVM fournit des interfaces pour initialiser les données des programmes et pour fournir les sorties. Ces interfaces sont écrites en Java. Elle fournit aussi des moyens pour charger des données XML permettant de valuer les variables abstraites du modèle.

Le programme exécuté par la BVM peut contenir des données ensemblistes et des substitutions indéterministes. Les propriétés du programme peuvent être vérifiées statiquement en utilisant l’Atelier B ou dynamiquement par la BVM lors de l’exécution des événements du programme. Cette nouvelle manière de programmer avec B offre de nouveaux potentiels, elle peut servir par exemple à prototyper rapidement un logiciel en utilisant toute la richesse du langage B, ou, autre exemple, à insérer au sein d’une application Java un module pour lequel on souhaiterait prouver des propriétés et qui serait développé avec la méthode formelle B.