next up previous
Next: Contents of the furniture Up : Table of contents Previous: Visulalisation of the B sources

Appuyer ici pour la version francaise.

DOWNLOAD THE PROJECT

The totality of the B development is available, which enables the comprehension of the various construction steps of the software, the testing of the Cash Dispensing Machine and the evaluation of the Atelier B's performances tools.

Owing to graphic simulator, present in the tar cabinet, you can execute and test the DAB.

Click here to dowload the compressed tar file.


next up previous
Next: The project in a few digits Up : table of contents Previous: Download the project

Appuyer ici pour la version francaise.

CONTENTS OF THE DOWNLOADABLE PACKAGE

The Atelier B is developed by Steria in cooperation with GEC ALSTHOM Transport, with the financing and collaboration of the RATP, the SNCF and the INRETS.

The code generated by the Atelier B

The Atelier B currently integrates two translators :

Both translations of the B development are available. Executables are available for SUN machines under UNIX, HP under UNIX and PC under linux. To generate executables for other target machines, one simply recompiles the sources, possibly by adapting the basic machines (see below).

The basic machines

In order to interface with the outside, the code generated by the Atelier B resorts to basic machines. There are 7 for this project.

These basic machines have been developed in C language for a SUN LX under Solaris 2. If it is wished to recompile the Cash Dispensing Machine for other targets, it is possible that adaptations will have to be brought to this code.

Only the basic machines in C language are provided; their parallel in Ada language will be available shortly.

Sources in B language

The Cash Dispensing Machine has been developed in B language using the Atelier B (version 2.8).

Joined documents

The documents provided are created automatically by the Atelier B. The documents are in Latex, Interleaf, Word and FrameMaker formats. These documents notably enable the visualisation of the project's architecture in the form of a graph, the results obtained on the proof and the dictionary of terms.

The project documentation

The provision comprises also the following documentation:

These documents are provided in Latex or PostScript format.

The Man Machine Interface

A simulator of the Cash Dispensing Machine is available; the Man/Machine Interface has been developed in Tcl/Tk.