B-Method


The B method is a method of software development based on B, a tool-supported formal method based on an abstract machine notation, used in the development of computer software.

Overview

B was originally developed in the 1980s by Jean-Raymond Abrial in France and the UK. B is related to the Z notation and supports development of programming language code from specifications. B has been used in major safety-critical system applications in Europe. It has robust, commercially available tool support for specification, design, proof and code generation.
Compared to Z, B is slightly more low-level and more focused on refinement to code rather than just formal specification — hence it is easier to correctly implement a specification written in B than one in Z. In particular, there is good tool support for this.
The same language is used in specification, design and programming.
Mechanisms include encapsulation and data locality.

Event-B

Subsequently, another formal method called Event-B has been developed based on the B-Method, support by the [|Rodin] Platform. Event-B is a formal method aimed at system-level modelling and analysis. Features of Event-B are the use of set theory for modelling, the use of refinement to represent systems at different levels of abstraction, and the use of mathematical proof for verifying consistency between these refinement levels.

The main components

The B notation depends on set theory and first order logic in order to specify different versions of software that covers the complete cycle of project development.

Abstract machine

In the first and the most abstract version, which is called the Abstract Machine, the designer should specify the goal of the design.

Refinement

  • Then, during a refinement step, they may pad the specification in order to clarify the goal or to turn the abstract machine more concrete by adding details about data structures and algorithms that define how the goal is achieved.
  • The new version, which is called Refinement, should be proven to be coherent and include all the properties of the abstract machine.
  • The designer may make use of B libraries in order to model data structures or to include or import existing components.

    Implementation

  • The refinement continues until a deterministic version is achieved: the Implementation.
  • During all of the development steps, the same notation is used, and the last version may be translated to a programming language for compilation.

    Software

B-Toolkit

The B-Toolkit is a collection of programming tools designed to support the use of the B-Tool, is a set theory-based mathematical interpreter for the purposes of supporting the B-Method. Development was originally undertaken by Ib Holm Sørensen and others, at BP Research and then at B-Core Limited.
The toolkit uses a custom X Window Motif Interface for GUI management and runs primarily on the Linux, Mac OS X and Solaris operating systems.
The B-Toolkit source code is now available.

Atelier B

Developed by ClearSy, Atelier B is an industrial tool that allows for the operational use of the B Method to develop defect-free proven software Community Edition, available to anyone without any restriction; 2) Maintenance Edition for maintenance contract holders only. Atelier B has been used to develop safety automatisms for the various subways installed throughout the world by Alstom and Siemens, and also for Common Criteria certification and the development of system models by ATMEL and STMicroelectronics.

Click'n'Prove

The Click'n'Prove tool provides an environment for the generation and discharge of proof obligations, for consistency and refinement checking.

Rodin

The Rodin Platform is a tool that supports Event-B. Rodin is based on an Eclipse software IDE and provides support for refinement and mathematical proof. The platform is open source and forms part of the Eclipse framework It is extendable using software component plug-ins. The development of Rodin has been supported by the European Union projects DEPLOY, RODIN, and ADVANCE.

BHDL

BHDL provides a method for the correct design of digital circuits, combining
the advantages of the hardware description language VHDL with the formality of B.

APCB

APCB has organized meetings associated with the B-Method. It has organized ZB conferences with the Z User Group and ABZ conferences, including Abstract State Machines as well as the Z notation.

Books

The following conferences have explicitly included the B-Method and/or Event-B: