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.

Compared to the Z notation, 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.

History

B was originally developed in the 1980s by Jean-Raymond Abrial in France and the UK. B is related to the Z notation (also originated by Abrial) and supports the development of programming language code from specifications. B has been used in major safety-critical system applications in Europe (such as the automatic Paris Métro lines 14 and 1 and the Ariane 5 rocket). It has robust, commercially available tool support for specification, design, proof and code generation.

Ib Holm Sørensen [dk], leader of the B-Toolkit development team and founder of B-Core

From the late 1980s, Ib Holm Sørensen [dk] (1949–2012) was central to the development of the B-Method, having previously also worked on the early development of the Z notation. He left the Oxford University Computing Laboratory to lead a team for BP Research and to develop the B-Toolkit, providing tool support for the B-Method. Subsequently, he founded the company B-Core (UK) Limited to support the B-Toolkit, which is a collection of programming tools designed to support the use of the B notation, and he helped to complete a number of B-related projects.

Event-B

Subsequently, another formal method called Event-B has been developed based on the B-Method, supported 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 to specify different levels of software description covering 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.

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

There are a number of software supporting the B-Method and Event-B.

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

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 (UK) 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 available on GitHub.

Click'n'Prove

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

ProB

ProB is a combined software animation tool and model checker for the B-Method. It enables the animation of many B specifications, and can also systematically check a specification for several types of errors. ProB includes constraint-solving facilities that can be used to aid in deadlock checking, model discovery, and test-case generation. The tool is developed by the STUPS group at the Heinrich Heine University Düsseldorf.

Rodin

The Rodin Platform is a tool that supports Event-B. Rodin is based on an Eclipse software IDE (integrated development environment) 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 (2008–2012), RODIN (2004–2007), and ADVANCE (2011–2014).

Others

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 (French: Association de Pilotage des Conférences B, the International B Conference Steering Committee) 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 (ASM) as well as the Z notation.

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

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

Z2B Conference, Nantes, France, 10–12 October 1995
First B Conference, Nantes, France, 25–27 November 1996
Second B Conference, Montpellier, France, 22–24 April 1998
ZB 2000, York, United Kingdom, 28 August – 2 September 2000
ZB 2002, Grenoble, France, 23–25 January 2002
ZB 2003, Turku, Finland, 4–6 June 2003
ZB 2005, Guildford, United Kingdom, 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 2008, BCS, London, United Kingdom, 16–18 September 2008
ABZ 2010, Orford, Québec, Canada, 23–25 February 2010
ABZ 2012, Pisa, Italy, 18–22 June 2012
ABZ 2014, Toulouse, France, 2–6 June 2014
ABZ 2016, Linz, Austria, 23–27 May 2016
ABZ 2018, Southampton, United Kingdom, 5–8 June 2018
ABZ 2020, Ulm, Germany, 9–13 June 2020 (delayed due to the COVID-19 pandemic)
ABZ 2021, Ulm, Germany, 9–13 June 2021
ABZ 2023, Nancy, France, 30 May – 2 June 2023
ABZ 2024, Bergamo, Italy, 25–28 2024
ABZ 2025, Düsseldorf, Germany, 10–13 June 2025
ABZ 2026, Tokyo, Japan, 18–20 May 2026

References

↑ Cansell, Dominique, and Dominique Méry. "Foundations of the B method." Computing and informatics 22, no. 3-4 (2003): 221-256.
↑ Butler, Michael, Philipp Körner, Sebastian Krings, Thierry Lecomte, Michael Leuschel, Luis-Fernando Mejia, and Laurent Voisin. "The first twenty-five years of industrial use of the B-method." In International Conference on Formal Methods for Industrial Critical Systems, pp. 189-209. Springer, Cham, 2020.
↑ Jean-Raymond Abrial (1988). "The B Tool (Abstract)" (PDF). In Bloomfield, Robin E.; Marshall, Lynn S.; Jones, Roger B. (eds.). VDM – The Way Ahead, Proc. 2nd VDM-Europe Symposium. Lecture Notes in Computer Science. Vol. 328. Springer. pp. 86–87. doi:10.1007/3-540-50214-9_8. ISBN 978-3-540-50214-2.
↑ Abrial, J-R., Matthew KO Lee, D. S. Neilson, P. N. Scharbach, and Ib Holm Sørensen. "The B-method." In International Symposium of VDM Europe, pp. 398-405. Springer, Berlin, Heidelberg, 1991.
↑ Bowen, Jonathan P.; Habrias, Henri (April–June 2025). "Jean-Raymond Abrial: A Scientific Biography of a Formal Methods Pioneer". IEEE Annals of the History of Computing. 48 (2). IEEE Computer Society: 71–80. arXiv:2604.07353. doi:10.1109/MAHC.2026.3685515.
↑ Gerhart, Susan, D. Craigen, and Ted Ralston. "Case study: Paris metro signaling system." IEEE Software 11, no. 1 (1994): 32-28.
↑ Behm, Patrick, Paul Benoit, Alain Faivre, and Jean-Marc Meynadier. "METEOR: A successful application of B in a large project." In International Symposium on Formal Methods, pp. 369-387. Springer, Berlin, Heidelberg, 1999.
↑ Lecomte, Thierry. "Applying a formal method in industry: a 15-year trajectory." In International workshop on formal methods for industrial critical systems, pp. 26-34. Springer, Berlin, Heidelberg, 2009.
↑ Bhattacharya, Sourav; Winter, Victor L., eds. (2012). "8. History of B". High Integrity Software. Springer. p. 40. ISBN 978-1461513919.
1 2 Bowen, Jonathan (July 2022). "Ib Holm Sørensen: Ten Years After" (PDF). FACS FACTS (2022–2). BCS-FACS: 41–49. Retrieved 3 August 2022.
↑ Crichton, Edward (29 March 2022). "BToolkit". GitHub.
↑ Roscoe, Bill (8 February 2012). "Ib Sorensen – In memoriam". Department of Computer Science, University of Oxford, UK.
↑ Wordsworth, J. B. (1996). Software Engineering With B. Addison-Wesley. ISBN 978-0201403565
1 2 3 "Event-B and the Rodin Platform". Event-B.org.
↑ Butler, Michael. "Decomposition structures for Event-B." In International Conference on Integrated Formal Methods, pp. 20-38. Springer, Berlin, Heidelberg, 2009.
↑ Abrial, Jean-Raymond. Modeling in Event-B: system and software engineering. Cambridge University Press, 2010.
1 2 Abrial, Jean-Raymond, Michael Butler, Stefan Hallerstede, Thai Son Hoang, Farhad Mehta, and Laurent Voisin. "Rodin: an open toolset for modelling and reasoning in Event-B." International Journal on Software Tools for Technology Transfer 12, no. 6 (2010): 447–466.
↑ Hoang, Thai Son, Andreas Fürst, and Jean-Raymond Abrial. "Event-B patterns and their tool support." Software & Systems Modeling 12, no. 2 (2013): 229–244.
↑ "AtelierB.eu".
↑ Mentré, David, Claude Marché, Jean-Christophe Filliâtre, and Masashi Asuka. "Discharging proof obligations from Atelier B using multiple automated provers." In International Conference on Abstract State Machines, Alloy, B, VDM, and Z, pp. 238-251. Springer, Berlin, Heidelberg, 2012.
↑ "The B-Toolkit". [B-Core (UK) Limited]. 2004. Archived from the original on October 12, 2004. Retrieved February 22, 2012.
↑ Haughton, Howard, and Kevin Lano. Specification in B: An introduction using the B toolkit. World Scientific, 1996.
↑ Abrial, Jean-Raymond. "The B Tool." In International Symposium of VDM Europe, pp. 86-87. Springer, Berlin, Heidelberg, 1988.
↑ B-Toolkit Requirements Archived 2004-10-12 at the Wayback Machine
↑ Crichton, Edward. "B-Toolkit source code". GitHub.
↑ Abrial, J.-R.; Cansell, D. (2003). "Click'n Prove: Interactive Proofs within Set Theory". In Basin, D.; Wolff, B. (eds.). Theorem Proving in Higher Order Logics (TPHOLs). Lecture Notes in Computer Science. Vol. 2758. Berlin, Heidelberg: Springer. doi:10.1007/10930755_1.
↑ "What is ProB?". Germany: Heinrich-Heine-Universität Düsseldorf. Retrieved 28 March 2026.
↑ "ProB?". railML.org. Retrieved 28 March 2026.
↑ Abrial, J-R. "A system development process with Event-B and the Rodin platform." In International Conference on Formal Engineering Methods, pp. 1–3. Springer, Berlin, Heidelberg, 2007.
↑ Aljer, Ammar, Philippe Devienne, Sophie Tison, J-L. Boulanger, and Georges Mariano. "BHDL: Circuit design in B." In Third International Conference on Application of Concurrency to System Design Proceedings, pp. 241–242. IEEE, 2003.
↑ "Association de pilotage des conférences B". librairiecosmopolite.com. Retrieved 27 July 2022.
↑ "Conferences". ABZ. Retrieved 16 January 2026.

External links

[1] Cansell, Dominique, and Dominique Méry. "Foundations of the B method." Computing and informatics 22, no. 3-4 (2003): 221-256.

[2] Butler, Michael, Philipp Körner, Sebastian Krings, Thierry Lecomte, Michael Leuschel, Luis-Fernando Mejia, and Laurent Voisin. "The first twenty-five years of industrial use of the B-method." In International Conference on Formal Methods for Industrial Critical Systems, pp. 189-209. Springer, Cham, 2020.

[3] Jean-Raymond Abrial (1988). "The B Tool (Abstract)" (PDF). In Bloomfield, Robin E.; Marshall, Lynn S.; Jones, Roger B. (eds.). VDM – The Way Ahead, Proc. 2nd VDM-Europe Symposium. Lecture Notes in Computer Science. Vol. 328. Springer. pp. 86–87. doi:10.1007/3-540-50214-9_8. ISBN 978-3-540-50214-2.

[4] Abrial, J-R., Matthew KO Lee, D. S. Neilson, P. N. Scharbach, and Ib Holm Sørensen. "The B-method." In International Symposium of VDM Europe, pp. 398-405. Springer, Berlin, Heidelberg, 1991.

[ieee-annals26-5] Bowen, Jonathan P.; Habrias, Henri (April–June 2025). "Jean-Raymond Abrial: A Scientific Biography of a Formal Methods Pioneer". IEEE Annals of the History of Computing. 48 (2). IEEE Computer Society: 71–80. arXiv:2604.07353. doi:10.1109/MAHC.2026.3685515.

[6] Gerhart, Susan, D. Craigen, and Ted Ralston. "Case study: Paris metro signaling system." IEEE Software 11, no. 1 (1994): 32-28.

[7] Behm, Patrick, Paul Benoit, Alain Faivre, and Jean-Marc Meynadier. "METEOR: A successful application of B in a large project." In International Symposium on Formal Methods, pp. 369-387. Springer, Berlin, Heidelberg, 1999.

[8] Lecomte, Thierry. "Applying a formal method in industry: a 15-year trajectory." In International workshop on formal methods for industrial critical systems, pp. 26-34. Springer, Berlin, Heidelberg, 2009.

[b12-9] Bhattacharya, Sourav; Winter, Victor L., eds. (2012). "8. History of B". High Integrity Software. Springer. p. 40. ISBN 978-1461513919.

[ihs22-10] 1 2 Bowen, Jonathan (July 2022). "Ib Holm Sørensen: Ten Years After" (PDF). FACS FACTS (2022–2). BCS-FACS: 41–49. Retrieved 3 August 2022.

[github-11] Crichton, Edward (29 March 2022). "BToolkit". GitHub.

[roscoe12-12] Roscoe, Bill (8 February 2012). "Ib Sorensen – In memoriam". Department of Computer Science, University of Oxford, UK.

[13] Wordsworth, J. B. (1996). Software Engineering With B. Addison-Wesley. ISBN 978-0201403565

[event-b-14] 1 2 3 "Event-B and the Rodin Platform". Event-B.org.

[15] Butler, Michael. "Decomposition structures for Event-B." In International Conference on Integrated Formal Methods, pp. 20-38. Springer, Berlin, Heidelberg, 2009.

[16] Abrial, Jean-Raymond. Modeling in Event-B: system and software engineering. Cambridge University Press, 2010.

[rodin10-17] 1 2 Abrial, Jean-Raymond, Michael Butler, Stefan Hallerstede, Thai Son Hoang, Farhad Mehta, and Laurent Voisin. "Rodin: an open toolset for modelling and reasoning in Event-B." International Journal on Software Tools for Technology Transfer 12, no. 6 (2010): 447–466.

[18] Hoang, Thai Son, Andreas Fürst, and Jean-Raymond Abrial. "Event-B patterns and their tool support." Software & Systems Modeling 12, no. 2 (2013): 229–244.

[19] "AtelierB.eu".

[20] Mentré, David, Claude Marché, Jean-Christophe Filliâtre, and Masashi Asuka. "Discharging proof obligations from Atelier B using multiple automated provers." In International Conference on Abstract State Machines, Alloy, B, VDM, and Z, pp. 238-251. Springer, Berlin, Heidelberg, 2012.

[21] "The B-Toolkit". [B-Core (UK) Limited]. 2004. Archived from the original on October 12, 2004. Retrieved February 22, 2012.

[22] Haughton, Howard, and Kevin Lano. Specification in B: An introduction using the B toolkit. World Scientific, 1996.

[23] Abrial, Jean-Raymond. "The B Tool." In International Symposium of VDM Europe, pp. 86-87. Springer, Berlin, Heidelberg, 1988.

[24] B-Toolkit Requirements Archived 2004-10-12 at the Wayback Machine

[25] Crichton, Edward. "B-Toolkit source code". GitHub.

[26] Abrial, J.-R.; Cansell, D. (2003). "Click'n Prove: Interactive Proofs within Set Theory". In Basin, D.; Wolff, B. (eds.). Theorem Proving in Higher Order Logics (TPHOLs). Lecture Notes in Computer Science. Vol. 2758. Berlin, Heidelberg: Springer. doi:10.1007/10930755_1.

[prob-27] "What is ProB?". Germany: Heinrich-Heine-Universität Düsseldorf. Retrieved 28 March 2026.

[28] "ProB?". railML.org. Retrieved 28 March 2026.

[29] Abrial, J-R. "A system development process with Event-B and the Rodin platform." In International Conference on Formal Engineering Methods, pp. 1–3. Springer, Berlin, Heidelberg, 2007.

[30] Aljer, Ammar, Philippe Devienne, Sophie Tison, J-L. Boulanger, and Georges Mariano. "BHDL: Circuit design in B." In Third International Conference on Application of Concurrency to System Design Proceedings, pp. 241–242. IEEE, 2003.

[31] "Association de pilotage des conférences B". librairiecosmopolite.com. Retrieved 27 July 2022.

[32] "Conferences". ABZ. Retrieved 16 January 2026.