Formal Methods

Z notation

B User Group

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).

• On-line resources
• Publications
• Tool support
• Projects
• Meetings

On-line resources

B User Group (BUG). Note: Activities have officially ceased since March 2000.

See also BUG phone book

Contact Georges Mariano for further BUG information.

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 on-line information concerning B, including information on the various B-Technologies

A mailing list for discussion about B has been established. Send an email message containing "subscribe b-talk" to b-talk-request@tees.ac.uk to join.

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!

Publications

Bibliographies

A list of references relevant to B is available on-line from the Z bibliography.

Both bibliographies are in BibTeX format suitable for use with the LaTeX document preparation system.

Books

• The B-Book: Assigning Programs to Meanings, J.-R. Abrial, Cambridge University Press, 1996. ISBN 0-521-49619-5. 850 pages. UK Price £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.

• The B-Method: An Introduction, Steve Schneider, Palgrave, Cornerstones of Computing series, October 2001. ISBN 0-333-79284-X. UK Price £29.99.

• Software Engineering with B, John Wordsworth, Addison Wesley Longman, 1996. ISBN 0-201-40356-0. US Price $50.82.

• The B Language and Method: A Guide to Practical Formal Development, Kevin Lano, Springer-Verlag, FACIT series, 1996. ISBN 3-540-76033-4. UK Price £29.50.

• Specification in B: An Introduction using the B Toolkit, Kevin Lano, World Scientific Publishing Company, Imperial College Press, 1996. ISBN 1-86094008-0.

Tool support

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).

Further information: Atelier B is composed of a complete set of integrated tools enabling the development of applications using the method invented by Jean-Raymond Abrial, the B-Method. Atelier B assists developers in the formalization of their aplications, performing automatically on specifications and their refinements, syntax analysis, type checking, generation and demonstration of proof obligations. Extra components are supplied such as translators into current computer programming languages (C, Ada, ...), a mathematical editor, libraries of predefined machines and various project analysis tools. Access to Atelier B software tools is by a graphical MOTIF interface or by a batch language; in each mode it manages multi-users projects. Atelier B has been designed by Digilog and GEC Alsthom Transport in close collaboration with Jean-Raymond Abrial. The first version of Atelier B will be upgraded in 1995 with an animator of specifications, a new generation of prover, a powerful project documentation generator and various interfaces with standard tools (SGML, Interleaf, ...). Atelier B is sponsored by RATP, SNCF and INRETS and developed with their technical co-operation.

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.

See also:

• A B editor for Unix/Motif on HP/Sun/SGI/DEC/Linux (information in French).

• Another's B Parser (in French and English).

• B fonts: True Type (zip format, for Windows) and PCF (tar format for Unix) from Bruno Tatibouët.

• RODIN B Sharp. See also links to other tools/projects.

• jBTools toolset including jBedit, an editor for B and a parser, transforming B to XML format. Uses Java.

• csp2B tool. Combination of CSP and B specifications by Michael Butler.

• ProB animator and model checker for the B-Method by Michael Leuschel.

• U2B: UML to B for Rational Rose.

Projects

• Brillant open source project. B: Recherches et Innovation à L'aide de Nouvelles Technologies.

• 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

1. 1st B Conference, Nantes, France, 25-27 November 1996.

2. B'98: 2nd International B Conference, Montpellier, France, 22-24 April 1998.
   See photographs.

3. FM'99: B-Method mini-track and User Group Meeting, Toulouse, France, 20-24 September 1999.

4. ZB2000: International Conference of B and Z Users, York, UK, 28 August - 2 September 2000.

5. 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.

6. One Day Workshop on B, Royal Holloway, University of London, UK, 14 July 2003. (See also 10 January 2002 event.)

7. ZB2003, Turku, Finland, 4-6 June 2003.

8. ZB2005, University of Surrey, UK, 13-15 April 2005. With cooperation between APCB and ZUG.

• Z notation and VDM (Vienna Development Method) for formal specification and development.

• A Comparison of Z and VDM with B/AMN (Abstract Machine Notation).

• B course by Prof. Henri Habrias (in French).

Part of the LSBU Museophile archive.