PRESENTATION : Atelier B tool

BART enables refinement and implementation generation using a refinement rule base that can be expanded by the user. BART operates on a refinement rule basis. Additional refinement rules can be added for refinement personalisation of certain components.

These are used to carry out all syntax verifications of files in B language:

• a model editor has been integrated into Atelier B. This integrates a syntax analyser, automatic completion as well as navigation functions throughout the model.
• the Type Checker first carries out a grammatical verification of a B component, and then a certain number of contextual verifications including the type control and the control of identifier scopes. Components have to pass through the Type Checker before being proved and before any other of the verifications presented below
• the B0 Checker carries out verifications specific to the BO language used in the installations (a sub-division of B language) to ensure that they can be translated.
  the project checker checks all the components of a project to control its architecture (the links between the components). The project must have been checked before the final translation of the project.

B models can be saved in pdf, rtf and LaTeX formats.

The installations make up the coding stage for a development in B language. They are written using a B language sub-assembly, similar to an imperative programming language. In order to facilitate code generation on any target system, the installations are translated automatically to standard programming language. The programmes obtained can then be compiled and assembled on the target machine to produce the executable software.

It is used for the graphic representation of the components of a project and their links, by positioning them automatically on the graph. The user can choose different display options, for example the type of links to be viewed, the view of the whole dependence graph of a project or the dependence graph of a component.

• the automatic generation of the proof obligations using the components in B language
• a B component is correct when its proof obligations are demonstrated
•  proof in automatic mode: most of the proof obligations are demonstrated without user intervention
• the proof in interactive mode used when the automatic mode has failed: the user guides the prover in its proof obligation demonstration using interactive commands (lemma additions, proof by case etc.)
• the predicate prover: predicate demonstration: demonstration of rules added by the user
• viewing poof obligations, their origin and their status (trivial, proved, non-proved)
• the management of a validated rule base including more than 2 200 rules

Atelier B offers large size project management services (including for example 500 components).

In particular :

• Atelier B used by several users in a network. These users can work on the same project at the same time
• to archive and restore a whole project
• to architecture a project or several sub-projects or libraries. As such, Atelier B enables large and modular developments by several developer teams
• to view the overall status of a project, by supplying for each component, its status (passed to Type Checker, translated to C or to Ada), the number of proof obligations and the percentage proved
• to generate automatically the dependencies between the project’s components. As such, to carry out an action (passage through the Type Checker, through the proof obligation generator etc.) on a selection of components, Atelier B reports the action(s) required for the components on which it depends.