Our tools

Atelier B


Atelier B is a tool enabling the operational use of B method. In a coherent environment, it provides many functions for managing projects in B language.

> VISIT THE WEB SITE: WWW.ATELIERB.EU

Functions


THESE FUNCTIONS CAN BE DIVIDED INTO FOUR CATEGORIES:

> proof aid, to demonstrate proof obligations using suitable proof tools
> development aid: automatic management of dependency between B components,
> user comfort tools: graphical representation of projects, display of project status and statistics, project archiving.

Use of Atelier B


Atelier B is either used via a Man Machine Interface in QT format or using the commands directly (command mode). Atelier B is multi-user. Tasks that can be automated during project development are the following:

> syntax verification of components
> automatic proof obligation generation
> automatic translation of B installations to C or Ada language

Currently, Atelier B is available in Windows, Linux, Mac OS and Solaris operating systems.