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. It was originally developed by Jean-Raymond Abrial in France and the UK. B is related to the Z notation (also originated by Abrial) and supports development of programming language code from specifications. B has been used in major safety-critical system applications in Europe (such as the Paris Métro Line 14). 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.

Recently, another formal method called Event-B[1] has been developed. Event-B is considered an evolution of B (also known as classical B). It is a simpler notation, which is easier to learn and use. It comes with tool support in the form of the Rodin tool.

The main components

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 Abstract Machine, the designer should specify the goal of the design.

Refinement

Implementation

Some B method characteristics

B-Toolkit

The B-Toolkit,[2] developed by Ib Holm Sørensen et al., is a collection of programming tools designed to support the use of the B-Tool, a set theory based mathematical interpreter, for the purposes of a formal software engineering methodology known as the B method.

The toolkit uses a custom X Window Motif Interface[3] for GUI management and runs primarily on the Linux, Mac OS X and Solaris operating systems. It has been developed by the UK based company B-Core (UK) Limited.[4]

The B-Toolkit source code is now available.[5]

Atelier B

Developed by ClearSy, Atelier B [6] is an industrial tool that allows for the operational use of the B Method to develop defect-free proven software (formal software). Two versions are available: Community Edition available to anyone without any restriction, Maintenance Edition for maintenance contract holders only.

It is 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.

Books

Conferences

See also

References

  1. Event-B.org — Event-B and the Rodin Platform.
  2. "The B-Toolkit". B-Core (UK) Limited. Archive.org. 2004. Archived from the original on October 12, 2004. Retrieved February 22, 2012. External link in |work= (help)
  3. B-Toolkit Requirements
  4. "B-Core (UK) Limited". Company Data Rex. Retrieved February 22, 2012.
  5. B-Toolkit source code
  6. "AtelierB.eu".

External links

This article is based on material taken from the Free On-line Dictionary of Computing prior to 1 November 2008 and incorporated under the "relicensing" terms of the GFDL, version 1.3 or later.

This article is issued from Wikipedia - version of the Friday, April 08, 2016. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.