B-Method

VL2 — Virtual Library
Computing
Software engineering
Formal methods
Z notation
B User Group

This document contains some pointers to information relating to the B-Method↑, and its associated tool support, available around the world on the World Wide Web (WWW).

Please add or correct information below. Alternatively, please contact Jonathan Bowen if you know of relevant online information not included here or would like to maintain information on a particular topic.

Conferences
ABZ 2021, 8th International Conference on Rigorous State Based Methods
Last B conference: B2007, 7th International B Conference, LIFC, Besancon, France, 17–19 January 2007
Last ZB conference: ZB2005, University of Surrey, UK, 13–15 April 2005

The B-Method↑ has been developed by Jean-Raymond Abrial↑ — also originator of the Z notation — and others. B is a formal method for the development of program code from a specification in the Abstract Machine Notation. It includes tool support and has been used in some significant industrial applications (e.g., by GEC Alsthom↑).

Online resources

Atelier-B, France.: B software development environment. See the boiler case study.

Information also available in French. See La Lettre B newsletter.

B-Core (UK) Limited, UK.: Markets the B-Toolkit.
Teesside B-Resource.: Provides much online information concerning B, including information on the various B-Technologies
Grenoble B Site.: Includes Actualités de B / B News, books, tools, projects, industrial and academic information, B Working Group, FAQ and links. Information in French and English. An excellent resource!
Event-B.org.: Site for Event-B and Rodin, an open-source toolset for Event-B.

Publications

Bibliographies

See the definitive B Bibliography

A searchable version is also available as part of the excellent Collection of Computer Science Bibliographies. The bibliography is in BibTeX format suitable for use with the LaTeX document preparation system.

Books

The following definitive book on B is available:

The B-Book: Assigning Programs to Meanings, J.-R. Abrial, Cambridge University Press, 1996. ISBN 0-521-49619-5. 850 pages. UK Price UK£40.00.

Contents: Mathematical reasoning; Set notation; Mathematical objects; Introduction to abstract machines; Formal definition of abstract machines; Theory of abstract machines; Construction large abstract machines; Example of abstract machines; Sequencing and loop; Programming examples; Refinement; Construction large software systems; Example of refinement;
Appendices: Summary of the most current notations; Syntax; Definitions; Visibility rules; Rules and axioms; Proof obligations.

Book reviews:

- Jonathan Bowen: B-hold the Future of Software Development. The Times Higher Education Supplement, Multimedia computer books, 1267:30, 14 February 1997.
- Michael Butler: Book Review, The Computer Journal, 40(1):59-61, 1997.

Tool support

The B-Tool is a language interpreter and a run-time environment for supporting B. The B-Toolkit is a set of integrated tools which fully supports the B-Method for formal software development, built on top of the B-Tool. These tools are available from B-Core (UK) Limited, UK. For further details, contact Ib Sørensen on b@b-core.com.

Atelier B, a tool supporting the Abstract Machine Notation (AMN), is available under licence. from ClearSy, France. Features include syntax, type and static semantics checking, proof support, refinement, a graphical interface and pretty-printing. An animator is planned. Test case generation is not supported. Contact Thierry Lecomte on contact@clearsy.com (tel: +33 4 42 37 12 70, fax: +33 4 42 37 12 71).

The B modeling environment B4free has been released and is now freely accessible to academics. B4free is a set of tools for the development of B models and for creation of user tools. The principal tool (bbatch) manages B projects. The Logic Solver (krt) is a compiler-interpreter for the Theory Language. All these tools are used in batch mode. A graphical interface, based on B4free and developed by Jean-Raymond Abrial and Dominique Cansell, is also available on the Click'n'Prove page.

Projects

EU IST MATISSE Project (2000-2003): Methodologies and Technologies for Industrial Strength Systems Engineering. Industrial case studies using B.
EU IST PUSSEE project: Paradigm Unifying System Specification Environments for proven Electronic design.
EU IST RODIN Project (2004–2007): Rigorous Open Development Environment for Complex Systems. See also RODIN B Sharp and SourceForge project information,
B User Trials (BUT) project and the MaFMeth Project (also supporting VDM-SL) at RAL and elsewhere in the UK, investigated the use of B.

Meetings

The International B Conference Steering Committee (Association de Pilotage des Conférences B — APCB) organizes the International B Conference:

1st B Conference, Nantes, France, 25–27 November 1996.
B'98: 2nd International B Conference, Montpellier, France, 22-24 April 1998.
See photographs.
FM'99: B-Method mini-track and User Group Meeting, Toulouse, France, 20–24 September 1999.
ZB2000: International Conference of B and Z Users, York, UK, 28 August – 2 September 2000.
ZB2002: International Conference of B and Z Users, Grenoble, France, 23–25 January 2002.
The local organizer was Didier Bert of the Laboratoire Logiciels Systèmes Réseaux (LSR), Instutute IMAG, Grenoble, who supported the event.
One Day Workshop on B, Royal Holloway, University of London, UK, 14 July 2003. (See also 10 January 2002 event.)
ZB2003, Turku, Finland, 4-6 June 2003.
ZB2005, University of Surrey, UK, 13–15 April 2005. With cooperation between APCB and ZUG.