Rahul Sharma (Editor)

B Method

Updated on
Edit
Like
Comment
Share on FacebookTweet on TwitterShare on LinkedInShare on Reddit

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.

Contents

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

  • Then, during a refinement step, he may pad the specification in order to clarify the goal or to turn the abstract machine more concrete by adding more details about data structures and algorithms that explain how the goal may be achieved.
  • The new version, which is called Refinement, should be proven to be coherent and including all the properties of the Abstract Machine.
  • Designer may make use of many B libraries in order to see data structure, to include or import some components.

    • Implementation

  • The refinement in its turn may be refined one or many times to obtain a deterministic version which is called Implementation.
  • During all of the development steps the same notation is used and the last version may be translated to Ada, C or C++ language.

    • Some B method characteristics

  • Use same language in specification, design and programming.
  • Mechanism include encapsulation and data locality.
  • Clear and close introduction for refinement concept.
  • Originated in the 1980s by Jean-Raymond Abrial.
  • B method is a tool-supported formal method based on AMN (Abstract Machine Notation), used in the development of correct software.
  • B method has been used in some major safety-critical system applications in Europe (such as in Paris Métro Line 14 and Ariane 5 rocket).

    • B-Toolkit

    The B-Toolkit, 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 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.

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

    Industrial use cases

    1998: Use on the metro line 14 in Paris (METEOR) by RATP Group. The embedded critical software has been modeled, proven and generated from formal specifications B.

    2005: RATP Group decide to automate line 1 (La défense / Vincennes) and to use B-method again.

    Books

  • The B-Book: Assigning Programs to Meanings, Jean-Raymond Abrial, Cambridge University Press, 1996. ISBN 0-521-49619-5.
  • The B-Method: An Introduction, Steve Schneider, Palgrave Macmillan, Cornerstones of Computing series, 2001. ISBN 0-333-79284-X.
  • Software Engineering with B, John Wordsworth, Addison Wesley Longman, 1996. ISBN 0-201-40356-0.
  • The B Language and Method: A Guide to Practical Formal Development, Kevin Lano, Springer-Verlag, FACIT series, 1996. ISBN 3-540-76033-4.
  • Specification in B: An Introduction using the B Toolkit, Kevin Lano, World Scientific Publishing Company, Imperial College Press, 1996. ISBN 1-86094-008-0.
  • Modeling in Event-B: System and Software Engineering, Jean-Raymond Abrial, Cambridge University Press, 2010. ISBN 978-0-521-89556-9.

    • Conferences

  • Conference Z2B, Nantes, France, oct. 10-12 1995
  • First B Conference, Nantes, France, nov. 25-27 1996
  • Second B Conference, Montpellier, France, ap. 22-24 1998,
  • ZB'2000, York, U.K., 28 aug, 2 sept. 2000,
  • ZB'2002, Grenoble, France, 23-25 jan. 2002,
  • ZB'2003, Turku, Finland, 4-6 jun. 2003
  • ZB'05, Guildford, U.K., 2005
  • B'2007, Besançon, France, 2007
  • B, from research to teaching, Nantes, France, 16 June 2008
  • B, from research to teaching, Nantes, France, 8 June 2009
  • B, from research to teaching, Nantes, France, 7 June 2010
  • ABZ conference: ABZ 2008, British Computer Society, London, UK, 16–18 September 2008
  • ABZ conference: ABZ 2010,Oxford, Québec, Canada, 23–25 February 2010
  • ABZ conference: ABZ 2012, Pisa, Italy, 18–22 June 2012
  • ABZ conference: ABZ 2014, Toulouse, France, 2–6 June 2014
  • ABZ conference: ABZ 2016, Linz, Austria, 23–27 May 2016

    • References

    B-Method Wikipedia
    (Text) CC BY-SA