Click here for English.
L'ensemble du développement B est disponible, ce qui permet de comprendre les différentes étapes de construction du logiciel, de tester le Distributeur Automatique de Billets et d'évaluer les performances des outils de l'Atelier B.
Gràce à un simulateur graphique, présent dans le fichier tar UNIX compressé, vous pouvez exécuter et tester le DAB.
Cliquer ici pour récupérer le fichier tar.
Click here for English.
L'Atelier B intègre actuellement deux traducteurs :
Les deux traductions du développement B sont disponibles. Des exécutables sont disponibles pour des machines SUN sous UNIX, HP sous UNIX et PC sous linux. Pour généner des exécutables pour d'autres machines cibles, il suffit de recompiler les sources, éventuellement en adaptant les machines de base (voir ci-dessous).
Afin de s'interfacer avec l'extérieur, le code généré par l'Atelier B fait appel à des machines de base. Elles sont au nombre de 7 pour ce projet.
Ces machines de base ont été développées en langage C pour une machine SUN LX sous Solaris 2. Si l'on souhaite recompiler le Distributeur Automatique de Billets pour d'autres cibles, il est possible que des adaptations devront être apportées à ce code.
Seules les machines de base en langage C sont fournies, leur correspondance en langage ADA sera disponible prochainement.
Le Distributeur Automatique de Billets a été développé en langage B en utilisant l'Atelier B (version 2.8).
Les documents fournis sont créés automatiquement par l'Atelier B. Les documents sont au format Latex, Interleaf, Word et FrameMaker. Ces documents permettent notamment de visualiser l'architecture du projet sous forme d'un graphe, les résultats obtenus sur la preuve et le dictionnaire des termes.
La fourniture comprend également la documentation suivante ;
Un simulateur du Distributeur Automatique de Billets est disponible; l'Interface Homme/Machine a été développée en Tcl/Tk.