Hubbry Logo
B-MethodB-MethodMain
Open search
B-Method
Community hub
B-Method
logo
7 pages, 0 posts
0 subscribers
Be the first to start a discussion here.
Be the first to start a discussion here.
B-Method
B-Method
B-Method
View on Wikipedia
from Wikipedia

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.[1][2]

Overview

[edit]

B was originally developed in the 1980s by Jean-Raymond Abrial[3][4] 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 automatic Paris Métro lines 14 and 1 and the Ariane 5 rocket).[5][6][7] 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

[edit]

Subsequently, another formal method called Event-B[8][9][10] has been developed based on the B-Method, support by the Rodin Platform.[11][12] 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

[edit]

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

[edit]

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

Refinement

[edit]
  • 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

[edit]
  • 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

[edit]

B-Toolkit

[edit]

The B-Toolkit[13][14] is a collection of programming tools designed to support the use of the B-Tool,[15] 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.[16]

The toolkit uses a custom X Window Motif Interface[17] for GUI management and runs primarily on the Linux, Mac OS X and Solaris operating systems.

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

Atelier B

[edit]

Developed by ClearSy, Atelier B[19][20] 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.

Click'n'Prove tool interface, an interactive theorem prover to assist with formal proofs using the B-Method

Click'n'Prove

[edit]

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

Rodin

[edit]
Main article: Rodin tool

The Rodin Platform is a tool that supports Event-B.[8][22][11] 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).[8]

BHDL

[edit]

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.[23]

APCB

[edit]

APCB (French: Association de Pilotage des Conférences B, the International B Conference Steering Committee) has organized meetings associated with the B-Method.[24] 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

[edit]
  • 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

[edit]

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, British Computer Society, 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, 2018
  • ABZ 2020, Ulm, Germany, 2021 (delayed due to the COVID-19 pandemic)
  • ABZ 2021, Ulm, Germany, 2021

See also

[edit]

References

[edit]
[edit]
Revisions and contributorsEdit on WikipediaRead on Wikipedia

B-Method

View on Grokipedia
from Grokipedia
The B-Method is a formal approach to software specification, design, and development that uses mathematical techniques to ensure system correctness and reliability, based on set theory, predicate calculus, and refinement principles. Invented by Jean-Raymond Abrial in the 1980s, it employs the B language—also known as Abstract Machine Notation (AMN)—to model systems as state-based machines, where operations are defined through generalized substitutions and invariants are proven to hold across refinements from abstract specifications to concrete implementations. The method's core strength lies in generating proof obligations that must be discharged to verify consistency, enabling fault-free software construction through stepwise refinement supported by tools like Atelier B and the B-Toolkit. Developed as a successor to earlier formal methods like Z, the B-Method was first systematically described in Abrial's The B-Book in 1996, building on Zermelo-Fraenkel with the to provide a rigorous foundation for modeling complex behaviors. Its classical form focuses on state-based specifications for sequential systems, but an event-based variant, Event-B, emerged in the early to better handle distributed and reactive systems by emphasizing events that trigger state changes while maintaining refinement and proof-based verification. Early adoption began in the French railway sector in the late 1980s, with the safety system for the Metro in 1989 marking one of the first industrial applications, followed by the fully automated driverless Metro Line 14 in , which involved over 115,000 lines of code and 27,800 proofs to achieve SIL4 safety integrity levels. The B-Method has seen widespread industrial use across safety-critical domains, including rail transport (e.g., Alstom's URBALIS 400 communication-based train control system, deployed in over 100 installations worldwide since 2008), aeronautics, automotive (e.g., vehicle modeling at Peugeot), smart cards for high-assurance security, defense, and nuclear systems. These applications demonstrate its ability to reduce testing efforts, simplify certification, and lower long-term development costs by formalizing requirements and enabling automatic code generation in languages like Ada or C. Tools such as Atelier B, used in more than 30% of communication-based metro systems, and open-source platforms like Rodin for Event-B, continue to support its evolution, with ongoing research addressing scalability and integration with other formalisms like CSP for concurrent systems.

Introduction

History and Development

The B-Method originated in the late as a formal approach to , primarily developed by Jean-Raymond Abrial as a successor to the , emphasizing refinement and tool-supported proof for rigorous specification and verification. Abrial, who had earlier contributed to while at the in the 1970s and , shifted focus to B to address limitations in handling implementation details through abstract machines and stepwise refinement. Initial formalization efforts in the involved collaborations among European researchers, building on mathematical foundations like to enable precise modeling of system behaviors. Key milestones in the 1990s marked B's transition from academic concept to practical toolset. In 1993, the first B-Toolset was delivered by , providing type-checking and proof capabilities that facilitated industrial application. Abrial's seminal publication, The B-Book: Assigning Programs to Meanings in 1996, formalized the method's principles, notations, and development process, serving as the authoritative reference for its use in specifying and coding software systems. By the late , B gained traction in safety-critical domains, notably through its adoption for the automatic train control system of , inaugurated in 1998, where over 110,000 lines of B models were used to generate 86,000 lines of Ada code, ensuring high reliability in a driverless rail environment. This project, led by RATP and partners like Matra Transport, demonstrated B's efficacy in rail signaling and extended to similar applications in and other sectors requiring certified software. In the , the method evolved into Event-B, an extension developed by Abrial to better support system-level modeling of discrete transition systems, incorporating event-driven refinements while retaining core B elements like set-theoretic notations. This transition, formalized in Abrial's 2010 book Modeling in Event-B: System and Software , broadened B's scope beyond software to complex reactive systems, influencing ongoing industrial uses in railways such as Alstom's URBALIS systems across multiple European cities. No formal international standardization emerged specifically for B, though its rigorous proof obligations contributed to sector-specific guidelines, such as those in European railway safety standards. The method's continued relevance is evident in recent projects, including the 2024 extension of , which relies on B for ensuring safety and reliability.

Core Principles

The B-Method embodies the correctness-by-construction paradigm, wherein systems are developed starting from highly abstract mathematical specifications that are progressively refined into executable code, with formal proofs ensuring that key properties—such as safety and functional correctness—are preserved at every step. This approach contrasts with traditional post-hoc verification by integrating proof obligations directly into the development process, thereby minimizing errors in safety-critical applications like railway signaling and avionics. By mandating exhaustive formal justification rather than partial or informal checks, the method avoids ambiguities that could lead to system failures, emphasizing a rigorous pathway from intent to implementation. At its foundation, the B-Method relies on Zermelo-Fraenkel with the (ZFC), providing a mathematically precise framework for modeling data and behaviors without reliance on ad-hoc assumptions. All variables in B specifications are treated as abstract sets, enabling the representation of complex structures—such as relations, functions, and sequences—through set-theoretic operations like unions, powersets, and Cartesian products, which underpin the method's expressive power. Operations, in turn, are formalized as generalized substitutions, a construct that generalizes classical assignment statements to include guarded actions, non-deterministic choices, and preconditioned behaviors, all defined within the weakest precondition semantics to ensure predictable state transitions. This set-theoretic rigor distinguishes the B-Method from informal engineering practices, as it requires full formal proofs of consistency and invariance preservation throughout the refinement process—often mechanized via tools that generate and discharge proof obligations automatically or interactively. Unlike methods that tolerate incomplete specifications or rely on testing alone, B insists on total coverage, making it particularly suited for domains where partiality could introduce unacceptable risks, such as embedded systems in transportation. Refinement serves as the mechanism to bridge abstraction levels while maintaining these guarantees, but the principles prioritize upfront mathematical certainty over iterative debugging.

Modeling Language

Abstract Machines

In the B-Method, an serves as the primary modeling artifact, encapsulating the state of a through variables and defining operations that transition between states in a modular and reusable manner. This structure enables of software behavior using and predicate logic, ensuring that all state changes preserve properties. The key components of an are organized into specific s within the Abstract Machine Notation (AMN). The names the and declares visibility to other machines via SEES or INCLUDES. The SETS clause defines deferred sets used in the model, while CONSTANTS and specify fixed values and their constraints. The VARIABLES clause declares state variables, the INVARIANT provides predicates that must hold for all reachable states, the INITIALISATION sets the starting state, and the OPERATIONS describes state-modifying actions using generalized substitutions with preconditions and postconditions. State in an abstract machine is represented by variables typed as basic sets (e.g., integers, booleans) or constructed types like relations, functions, or sequences, ensuring without implementation details. Invariants are logical predicates over these variables that guarantee consistency, such as type constraints or relational properties, and must be maintained by every operation to uphold the machine's correctness. A representative example is a simple counter machine, which models a bounded value with increment and decrement operations:

MACHINE Counter SEES Short CONSTANTS max_val PROPERTIES max_val ∈ SHORT ∧ max_val > 0 VARIABLES value INVARIANT value ∈ SHORT ∧ value ≤ max_val INITIALISATION value := 0 OPERATIONS increment(n) = PRE n ∈ SHORT ∧ n > 0 ∧ value + n ≤ max_val THEN value := value + n END; decrement = PRE value > 0 THEN value := value − 1 END; res ← getValue = BEGIN res := value END END

MACHINE Counter SEES Short CONSTANTS max_val PROPERTIES max_val ∈ SHORT ∧ max_val > 0 VARIABLES value INVARIANT value ∈ SHORT ∧ value ≤ max_val INITIALISATION value := 0 OPERATIONS increment(n) = PRE n ∈ SHORT ∧ n > 0 ∧ value + n ≤ max_val THEN value := value + n END; decrement = PRE value > 0 THEN value := value − 1 END; res ← getValue = BEGIN res := value END END

Here, value represents the counter state, the invariant ensures it stays non-negative and bounded, initialization sets it to zero, and operations include guards to prevent invalid states. Abstract machines promote modularity by allowing one machine to SEE another's constants and variables for read-only access or INCLUDE it for shared state, facilitating composition into larger systems without direct coupling. This design supports refinement, where abstract machines are progressively detailed toward concrete implementations while preserving invariants.

Notations and Syntax

The B-Method employs a formal notation grounded in and predicate logic to specify abstract machines and their behaviors, enabling precise mathematical descriptions of system states and operations. This notation includes symbols for sets, relations, and logical predicates, which are used to declare types, invariants, and substitutions within machine specifications. Basic notations in B-Method draw from , featuring symbols such as ∈\in for membership, ⊆\subseteq for inclusion, ∪\cup for union, ∩\cap for , and ×\times for Cartesian products. Predicate logic notations include ∀\forall, ∃\exists, conjunction ∧\wedge, disjunction ∨\vee, and implication ⇒\Rightarrow, allowing the expression of constraints and properties in a rigorous manner. For instance, a predicate might state ∀x∈Z⋅(x>0⇒P(x))\forall x \in \mathbb{Z} \cdot (x > 0 \Rightarrow P(x)), where Z\mathbb{Z} denotes the set of integers. Substitution notations facilitate the description of state transitions, with structures like ANY x WHERE P THEN S END\mathbf{ANY}\ x\ \mathbf{WHERE}\ P\ \mathbf{THEN}\ S\ \mathbf{END} for non-deterministic choices over variables xx satisfying predicate PP, followed by substitution SS. use PRE P THEN S END\mathbf{PRE}\ P\ \mathbf{THEN}\ S\ \mathbf{END}, executing SS only if PP holds. These are essential for defining operations that modify machine variables while preserving invariants. Type declarations specify the domains of variables and expressions, using typed sets such as P(1..n)\mathbb{P}(1..n) for the powerset of integers from 1 to nn, and relations denoted by ↔\leftrightarrow, partial functions by →\to, and total functions by ↠\twoheadrightarrow. Predefined types include Z\mathbb{Z} for integers, N\mathbb{N} for natural numbers, R\mathbb{R} for reals, BOOL\mathrm{BOOL} for Booleans, and STRING\mathrm{STRING} for strings, with powersets like P(T)\mathbb{P}(T) for any type TT. Deferred sets are declared in the SETS\mathbf{SETS} clause as identifiers, optionally enumerated via VALUES\mathbf{VALUES}, ensuring in specifications. The syntax for key clauses follows structured rules akin to BNF, where the INVARIANT\mathbf{INVARIANT} clause consists of one or more predicates conjoined by ∧\wedge, such as var∈NAT∧var>0\mathrm{var} \in \mathbb{NAT} \wedge \mathrm{var} > 0, defining state constraints. Operations in the OPERATIONS\mathbf{OPERATIONS} clause are defined as op(input)={PRE P THEN S END\mathrm{op}(\mathrm{input}) = \begin{cases} \mathbf{PRE}\ P\ \mathbf{THEN}\ S\ \mathbf{END} \end{cases} or op←op_call\mathrm{op} \leftarrow \mathrm{op\_call}, with inputs typed in the precondition PP and outputs via substitution SS, ensuring no variable renaming in abstract machines. Common constructs include Cartesian products T×UT \times U, typed as P(T×U)\mathbb{P}(T \times U), for pairing elements from types TT and UU. Functions are partial (E→FE \to F) or total (E↠FE \twoheadrightarrow F), both typed as P(E×F)\mathbb{P}(E \times F), with application as f(x)f(x). Sequences, denoted seq(T)\mathrm{seq}(T), support operations like first\mathrm{first}, last\mathrm{last}, front\mathrm{front}, and tail\mathrm{tail} for ordered collections.
ConstructNotationType/Example
Cartesian ProductT×UT \times UP(T×U)\mathbb{P}(T \times U), e.g., (1..12)×Z(1..12) \times \mathbb{Z}
Total FunctionE↠FE \twoheadrightarrow FP(E×F)\mathbb{P}(E \times F), e.g., (1..12)↠Z(1..12) \twoheadrightarrow \mathbb{Z}
Partial FunctionE→FE \to FP(E×F)\mathbb{P}(E \times F)
Sequenceseq(E)\mathrm{seq}(E)seq(E)\mathrm{seq}(E), e.g., seq(1,2,3)\mathrm{seq}(1,2,3)

Refinement and Verification

Refinement Steps

In the B-Method, refinement defines a simulation relation between an abstract machine AA and a concrete machine CC, ensuring that CC preserves the observable behaviors of AA while incorporating additional implementation details. This relation allows for the gradual development of a system from a high-level specification to a more detailed model, maintaining correctness at each stage. The core idea is that every execution trace of CC must correspond to a valid trace in AA, preventing the introduction of new errors or inconsistencies. Central to this process is the gluing invariant, a predicate J(x,y)J(x, y) that relates the abstract variables xx (from AA) to the concrete variables yy (from CC), such as y=f(x)y = f(x) for some function ff. This invariant ensures that the concrete state always represents a valid abstraction of the abstract state, and it must hold initially and be preserved by all concrete operations. By enforcing this link, the gluing invariant facilitates the verification that refinements do not violate the abstract model's properties. Refinement in the B-Method includes two primary types: data refinement, which elaborates the state space by replacing abstract data structures with more concrete representations (e.g., sets with arrays for ), and operation refinement, which simulates abstract events through concrete operations, potentially strengthening guards or specifying non-deterministic choices. Data refinement focuses on representational changes without altering behavioral semantics, while operation refinement ensures that concrete actions mimic the input-output relations of their abstract counterparts. These types can be combined within a single refinement step to progressively concretize both data and behavior. Validating a refinement involves proving three key aspects: simulation, where concrete operations provide witnesses for abstract outputs to confirm behavioral equivalence; data preservation, which verifies that the gluing invariant is maintained across operation executions; and non-divergence, ensuring the concrete machine avoids infinite loops or stuttering that could undermine progress in the abstract model. These proofs rely on discharging specific obligations, such as initial state compatibility and invariant preservation after each event. Multi-level refinement extends this process into a chain of successive models, where each concrete machine serves as the abstract basis for the next refinement, enabling a stepwise descent from specification to code. For instance, an initial abstract model of a computation might be refined first to introduce control structures and then further to algorithmic details, with each level's gluing invariant linking back to the original specification. This hierarchical approach supports modular development and reuse, as verified at every transition.

Proof Obligations

In the B-Method, proof obligations are formal statements that must be verified to ensure the consistency and correctness of abstract machines, refinements, and implementations. These obligations are automatically generated from the model's clauses, such as invariants, preconditions, and substitutions, to confirm that the specified system behaves as intended. The primary types of proof obligations include invariant preservation, which requires that every operation maintains the machine's invariants; initialization correctness, ensuring the initial state satisfies the invariants; operation guards, verifying that preconditions are respected; and for refinements, confirming that operations correctly simulate their abstract counterparts. These obligations are categorized into properties, which focus on preserving invariants and postconditions to keep the system in valid states, and progress properties, which involve variants to ensure termination and avoid infinite loops. Formally, for an operation SS with precondition pre(S)\text{pre}(S), invariant preservation is expressed as {pre(S)⇒wp(S,invariant)}\{\text{pre}(S) \Rightarrow \text{wp}(S, \text{invariant})\}, where wp\text{wp} denotes the weakest precondition that guarantees the invariant holds after the substitution in SS. Similarly, initialization obligations take the form ⇒[initial substitution](invariant)\Rightarrow [\text{initial substitution}](\text{invariant}), ensuring the starting state upholds all invariants. For refinements, simulation obligations use a double implication to verify that the gluing invariant links abstract and concrete behaviors without contradiction. Proof obligations are discharged through manual proofs in , often using substitutions and inference rules, or via automated provers that apply tactics to statements. For example, consider a simple tracking a sum of values with invariant sum≤total\text{sum} \leq \text{total}; after an operation SS that increments sum\text{sum} by 1 under sum<total\text{sum} < \text{total}, the obligation requires proving sum<total⇒[sum:=sum+1](sum≤total)\text{sum} < \text{total} \Rightarrow [\text{sum} := \text{sum} + 1](\text{sum} \leq \text{total}), which holds by arithmetic reasoning. These obligations play a central role in the B-Method's verification process by providing a systematic way to check model properties before implementation.

Development Process

Specification Phase

The specification phase in the B-Method initiates the formal development lifecycle by translating high-level requirements into a using Abstract Machine Notation (AMN). This phase focuses on capturing functional requirements through the definition of an abstract machine, which encapsulates the system's state and behavior without reference to implementation details. Engineers identify key variables representing the state, establish invariants that constrain possible states to ensure correctness, and define operations that describe state transitions based on preconditions and postconditions. For instance, in modeling a departure check system, variables such as speed and emergency-brake status are declared, with invariants ensuring speed is a , and operations like activating departure only when speed equals zero. Best practices emphasize starting with high-level functional specifications to maintain , employing and predicate calculus for precise requirement articulation. For large systems, techniques—such as inclusion or shared variable components—are recommended to modularize the model, allowing parallel development of subsystems while preserving overall consistency through gluing invariants in refinements. Proof obligations are generated early to verify that initialization establishes invariants and that operations preserve them, often using tools for automated checking. Outputs include a verified abstract model, typically comprising a few hundred lines for simple systems or thousands for complex ones, with all invariants proven to hold, providing a rigorous foundation for subsequent phases. Challenges in this phase include balancing sufficient abstraction to avoid premature design decisions with completeness to cover all requirements, particularly for non-functional aspects like timing, which the core B-Method handles indirectly through discrete models rather than real-time constraints. Handling timing requires extensions or separate analyses, as the method primarily targets functional correctness in sequential systems. In safety-critical domains like avionics, the specification aligns with DO-178B/C standards by generating traceable proof obligations that support verification objectives, such as substituting formal proofs for some testing activities when using qualified tools like Atelier B. This phase transitions briefly to refinement by providing the abstract model as a baseline for gradual concretization.

Implementation Phase

The implementation phase of the B-Method involves translating the most concrete abstract machine, known as the implementation level, into executable code through dedicated code generators integrated into tools like Atelier B. This phase relies on the prior refinement process, where abstract specifications are progressively concretized to ensure the final model is deterministic and suitable for programming. The code generation applies a direct, one-to-one mapping from the B0 subset of the B language—which restricts operations to implementable, deterministic substitutions—to target programming constructs, thereby preserving the formal properties established in earlier phases. In this translation, substitutions in the B implementation are converted to equivalent imperative statements, such as conditional branches for selections, loops for repetitions, and assignments for atomic actions, without introducing additional logic or optimizations that could compromise provable correctness. Non-determinism, present in abstract models, is systematically resolved through the refinement chain, ensuring the concrete machine contains only deterministic choices that map straightforwardly to sequential code; for instance, non-deterministic ANY substitutions are refined into specific deterministic forms like FORALL or explicit conditionals. This rule-based approach, devoid of "intelligence" in the generators, facilitates manual verification of the output against the B model. Validation of the generated code is achieved through the transitivity of the refinement proofs: since each refinement step from the initial abstract machine to the concrete implementation has been formally proven for consistency and well-implementation—covering invariants, safety properties, and data refinement—the resulting code inherits satisfaction of the original specification without requiring separate proofs on the code itself. Tools like Atelier B automate these proof obligations, confirming that the code upholds the system's behavioral semantics. For safety-critical applications, this formal assurance targets high integrity levels, such as SIL3/SIL4 under IEC 61508, where failure rates below 10^{-7} to 10^{-9} per hour are mandated. Supported target languages include via the ComenC translator, Ada 95, and High Integrity Ada for embedded systems, with extensions to through the B4SYN tool for hardware description in real-time contexts, such as microcircuits up to 5,000 gates, and code for programmable logic controllers like S7 . These generators produce compilable directly from the B implementation, as exemplified in projects like the flight software, where 80 lines of Ada were generated from a refined Event-B model. Following code generation, is performed to verify interactions with non-B components, such as using testbenches for outputs or comparing generated code against handwritten equivalents, though the B-Method prioritizes exhaustive over empirical testing to minimize residual errors. This post-implementation step ensures deployability in industrial environments while leveraging the method's correctness-by-construction paradigm.

Tools and Environments

Commercial Tools

Atelier B, developed by CLEARSY (formerly associated with Steria), is a comprehensive (IDE) for the B-Method, supporting the full software lifecycle from abstract specification to certified code generation. It enables formal modeling using B and Event-B notations, automatic proof obligation generation, interactive and automatic theorem proving, and animation for validation, with integration options for tools like to enhance proof automation and . Widely adopted in safety-critical domains, Atelier B has been instrumental in rail signaling projects, including the development of driverless metro systems in and other European cities, where it facilitates mathematically proven software to meet stringent reliability requirements. As of January 2025, Atelier B has achieved T2 certification under EN 50128 and , enabling its use in applications requiring high safety integrity levels such as SIL4. The B-Toolkit, originally developed at the and commercialized by B-Core (UK) Limited, provides a suite of tools for B-Method-based formal , including syntax and type checking, proof obligation generation, automated and interactive proving, animation, and code generation for languages like and Ada. It supports the entire refinement process from abstract machines to concrete implementations, with features for consistency checking and simulation to verify system behavior early in development. The toolkit has been used in industrial pilots for high-assurance systems, emphasizing rigorous verification through mechanical support for proofs. Click'n'Prove, developed by Jean-Raymond Abrial and collaborators associated with INRIA, is an interactive tailored for discharging B-Method proof obligations within , offering a user-friendly graphical interface for step-by-step proof construction and automation via underlying provers like the Predicate Prover. It focuses on making formal proofs accessible by allowing users to explore and justify obligations interactively, complementing automatic tools in complex developments. Several B-Method tools, notably Atelier B, achieve certification under standards such as at 4 (SIL4), enabling their use in applications requiring the highest risk reduction, including railway systems compliant with EN 50128. These certifications validate the tools' reliability for generating proven artifacts in certified toolchains, distinguishing them from open-source alternatives like Rodin by providing industrial-grade support and compliance documentation.

Open-Source Tools

The Rodin platform is an open-source, Eclipse-based originating from the European DEPLOY , primarily designed for modeling and reasoning in Event-B—a formal method evolved from the B-Method—but extensible via plugins to support B-Method workflows. It facilitates refinement-based development through graphical editors for abstract machines, automated proof obligation generation, and interactive theorem proving using back-end provers like Rodin PP and external tools such as Z3. Key features include collaborative modeling via integration with systems like SVN for team-based development, enabling shared repositories and concurrent editing of models. Additionally, Rodin incorporates the model checker as a plugin for validation, supporting and exhaustive checking of B-Method and Event-B models. ProB serves as an animator and validator specifically tailored for B-Method models, leveraging constraint-solving techniques based on to simulate model behaviors and detect inconsistencies. Developed at , it allows users to interactively explore abstract machines by executing operations step-by-step, generating counterexamples for unreachable states, and performing to verify properties like deadlock freedom without requiring full proof efforts. ProB integrates seamlessly as a Rodin plugin, enhancing its utility for B-Method users by providing both forward and backward modes, and it supports extensions for custom constraint solvers to handle complex data types common in B specifications. The tool has been applied in academic settings to validate safety-critical systems, demonstrating its effectiveness in early error detection through automated analysis. Community-driven extensions further enrich open-source support for B-Method, including the UML-B plugin for Rodin, which offers a graphical, UML-like notation for specifying Event-B models with class diagrams, state machines, and sequence diagrams that translate directly into B-Method-compatible abstract machines. This integration bridges informal UML modeling with formal B semantics, aiding accessibility for developers familiar with object-oriented paradigms. Open proof libraries, such as those embedded in Rodin for and refinement calculus, provide reusable lemmas and tactics for discharging proof obligations, with community-contributed extensions like the Qualitative Probability library supporting probabilistic termination proofs. Other notable open-source tools include the BToolkit, a comprehensive suite for B-Method development featuring static analysis, simulation, and theorem proving, distributed under a BSD . These open-source tools offer significant advantages for academic and applications, providing free access to advanced formal modeling capabilities and seamless integration with modern IDEs like Eclipse, which fosters extensibility through a plugin ecosystem. Their open nature encourages community contributions, such as custom provers and libraries, democratizing B-Method adoption beyond industrial constraints. However, they place less emphasis on certified code generation and industrial-scale certification compared to commercial tools, potentially limiting deployment in highly regulated domains without additional validation steps.

Applications and Extensions

Industrial Applications

The B-Method has been extensively applied in the rail sector for developing safety-critical signaling and control systems. A seminal example is the , inaugurated in 1998, where (formerly ) employed the full B-Method for the automatic train control software, encompassing over 115,000 lines of code and 27,800 proofs, with only 8.1% requiring manual intervention. This driverless system has operated without any software-related incidents since deployment, demonstrating the method's reliability in achieving SIL4 certification for and train control. The project's success led to its extension, still relying on B-Method-verified software for enhanced safety and interoperability. In , the B-Method supports certification under for embedded systems in safety-critical environments. It was used for the Roissy-Charles de Gaulle Airport shuttle (), operational since 2007, involving 183,000 lines of and 43,610 proofs, resulting in error-free performance with no anomalies reported. The automotive industry has leveraged the B-Method for systems, particularly in vehicles. In a five-year collaboration with PSA , B-Method models covered 52 embedded functions across 30,000 lines of , enabling that improved fault diagnosis efficiency and supported certification to requirements. Model reuse in this project reduced subsequent development time by a factor of three compared to initial efforts. Case studies highlight the B-Method's impact on defect reduction and cost efficiency. For , formal proofs eliminated the need for , yielding software with zero defects post-validation and no updates required in over two decades. The B-Method was applied in the New York Canarsie Line signaling upgrade, where safety-critical parts were developed using automatic refinement tools. By , the method underpinned over 100 industrial installations worldwide, primarily in rail signaling via systems like Alstom's URBALIS 400. Event-B represents a significant evolution of the B-Method, developed by Jean-Raymond Abrial in the 2000s as its direct successor. Unlike the B-Method's emphasis on stepwise refinement from abstract specifications to executable code, Event-B replaces traditional refinement chains with a more flexible event-based modeling approach, where system behavior is described through guarded events and explicit proof obligations for consistency and safety properties. This shift enables better handling of system-level design, including distributed systems, and is supported by the Rodin tool platform for automated proof and model checking. The B-Method shares a set-theoretic foundation with the , both drawing from and for . However, while Z prioritizes high-level, mathematical descriptions of system properties without a built-in path to , the B-Method integrates refinement directly into its core process, allowing specifications to be progressively concretized into code through abstract machines and proof obligations. This makes B more operational and tool-oriented for development, contrasting Z's focus on specification validation via theorem proving or testing. In comparison to the (VDM), the B-Method employs a weaker system where sets serve as the primary mechanism for defining types, with all sets implicitly finite, whereas VDM provides more structured, explicit type definitions including higher-order functions and stronger static checking. Relative to , a lightweight for , B-Method is more operational, emphasizing refinement toward imperative code generation rather than Alloy's relational logic for automated bounded model finding and detection. Extensions of the B-Method include UML-B, a graphical notation that incorporates UML-like diagrams for class and state machine modeling while maintaining formal semantics through translation to B or Event-B machines, facilitating object-oriented design. Additionally, integrations with the Analyzer allow encoding B specifications for , enhancing verification of properties like deadlock freedom. Many practitioners have transitioned from the B-Method to Event-B to leverage its improved scalability for larger, system-wide models, with tools like Atelier B now supporting both to ease adoption.

Literature and Community

Key Publications

The B-Book: Assigning Programs to Meanings by J.-R. Abrial, published in 1996 by , serves as the foundational comprehensive reference for the B-Method, detailing its abstract machine notation, semantics based on and predicate calculus, and the principles of refinement for rigorous . This text establishes the for specifying, designing, and verifying programs, emphasizing mathematical correctness from abstract specifications to concrete implementations. Software Engineering with B by J.B. Wordsworth, published in 1996 by , provides a practical on applying the B-Method in industrial settings, focusing on its use for developing safety-critical systems through stepwise refinement and tool-supported verification. The book illustrates how B's abstract machines facilitate structured processes, including case studies on real-world projects to demonstrate feasibility and benefits in professional environments. Key early papers include J.-R. Abrial's 1980 report on the CIP (Constructive Implementation of Programs) language, which laid the groundwork for B-Method by introducing rigorous specification techniques using predicate logic and for program construction. Abrial's 1996 work in The B-Book further formalized the refinement calculus, defining precise proof obligations for data and operation refinement to ensure consistency across development levels. A more recent publication, Modeling in Event-B: System and Software Engineering by (2010, ), extends the B-Method into Event-B, offering a refined approach to modeling complex systems with emphasis on event-driven refinements and automated proof. This book bridges classical B to modern applications by introducing rodin tools for refinement and validation, while preserving core semantic principles.

Conferences and Standards

The B-method community initially organized a series of dedicated international conferences known as the B Conferences, held from 1995 to 2007 under the auspices of the APCB (Association de Pilotage des Conférences B). These events focused on advances in the B-method, tool support, and industrial applications, with the first conference (B'95) in , , and the second (B'98) in Montpellier, , featuring refereed proceedings on topics such as and verification. Since 2008, B-method research has been integrated into the ABZ conference series (Abstract State Machines, , B, and ), which promotes cross-fertilization among state-based . The inaugural ABZ conference was held in in 2008, followed by the second in Orford, Canada, in 2010, with subsequent editions biennially emphasizing rigorous modeling and proof techniques involving B. B-method contributions also appear regularly in the broader International Symposium on (FM) series, a biennial event covering diverse formal techniques since 1991, where papers on B-based verification and refinement have been presented to advance system correctness. Workshops complement these conferences, particularly the annual Rodin User and Developer Workshops, which target the Rodin platform for Event-B (an evolution of the B-method). These gatherings emphasize practical tool usage, plug-in developments, and case studies from industrial projects, with the 11th edition held in 2024 in , , featuring proceedings on modeling challenges and extensions, and the 12th edition held on June 10, 2025, in , . On standards, the APCB serves as the steering body for B-method events and promotes , including processes for B tools to ensure reliability in critical systems. B-method tools and practices align with standards such as EN 50128 for software, enabling development of SIL 4-compliant systems like signaling and control applications. Similarly, B-method approaches support compliance with for automotive , through in high-ASIL contexts, as recommended for semi-formal and formal techniques in the standard. The B-method community, including industrial practitioners, contributes to formal methods standards bodies via groups like the APCB and participation in workshops such as FMICS (Formal Methods for Industrial Critical Systems), fostering alignment with sector-specific regulations.

References

  1. https://homepage.cs.uiowa.edu/~tinelli/classes/181/Papers/cai-b.pdf
  2. https://www.atelierb.eu/en/presentation-of-the-b-method/
  3. https://dl.acm.org/doi/10.5555/525749
  4. https://www.krin.gs/publication/butler-history-of-b-fmics20/butler-history-of-b-fmics20.pdf
  5. https://www.event-b.org/
  6. https://www.krin.gs/publication/krings-history-of-b-hfm19/krings-history-of-b-hfm19.pdf
  7. https://www.cs.ru.nl/~freek/courses/pa-2016/slides/MethodB.pdf
  8. https://www.clearsy.com/en/the-tools/extension-of-line-14-of-the-paris-metro-over-25-years-of-reliability-thanks-to-the-b-formal-method/
  9. https://www.atelierb.eu/wp-content/uploads/2023/07/B_EventB_JRA.pdf
  10. https://hal.science/inria-00099794
  11. https://cai.type.sk/content/2003/3-4/foundations-of-the-b-method/
  12. http://www.imm.dtu.dk/~db/cai/cai-b.pdf
  13. https://cgi.cse.unsw.edu.au/~cs2111/ClassicalB/PDF/intro-b-method-article.pdf
  14. https://stlab.dinfo.unifi.it/fantechi/INFIND/onlyB.pdf
  15. https://www.cai.sk/ojs/index.php/cai/article/download/456/364/1444
  16. https://www.atelierb.eu/wp-content/uploads/2023/02/2006-AutomationofJavaCardcomponentdevelopmentusingtheBmethod.pdf
  17. https://www.atelierb.eu/wp-content/uploads/2023/10/b-language-reference-manual.pdf
  18. https://link.springer.com/content/pdf/10.1007/BFb0053355
  19. https://centralesupelec.hal.science/hal-00292648/document
  20. https://im.ntu.edu.tw/~tsay/dokuwiki/lib/exe/fetch.php?media=courses:ssv2010:b.pdf
  21. https://www.math.pku.edu.cn/teachers/qiuzy/fm_B/Atelier_B/proof-obligations-reference.pdf
  22. https://www.cambridge.org/core/books/bbook/proof-obligations/1BA731A9611F76611F40FABF66093286
  23. https://link.springer.com/content/pdf/10.1007/10720327_2.pdf
  24. https://www.atelierb.eu/en/presentation-of-the-b-method/formal-proof-presentation/
  25. https://proglang.informatik.uni-freiburg.de/teaching/swt/2013/w04-b-method.pdf
  26. http://web1.see.asso.fr/erts2012/Site/0P2RUC89/5C-2.pdf
  27. https://www.atelierb.eu/wp-content/uploads/2021/03/6-code-generation.pdf
  28. https://www.atelierb.eu/en/presentation-of-the-b-method/generation-code-copy/
  29. https://www.atelierb.eu/en/atelier-b-tools/
  30. https://www.clearsy.com/en/tools/atelier-b/
  31. https://www.atelierb.eu/en/
  32. https://www.clearsy.com/en/the-tools/t2-certification-for-atelier-b/
  33. https://www.clearsy.com/en/thematics/b-method/
  34. https://dl.acm.org/doi/10.1007/978-3-030-58298-2_8
  35. https://www.linkedin.com/posts/clearsy_formal-programming-formalmethods-activity-7023930833883258881-X3Aq
  36. https://www.cs.ox.ac.uk/softeng/subjects/MAS.html
  37. https://link.springer.com/content/pdf/10.1007/3-540-59293-8_243.pdf
  38. https://cgi.cse.unsw.edu.au/~reports/papers/0620.pdf
  39. https://www.researchgate.net/publication/221302177_Click%27n%27Prove_Interactive_Proofs_Within_Set_Theory
  40. https://link.springer.com/chapter/10.1007/10930755_1
  41. https://www.southampton.ac.uk/~tsh2n14/publications/journals/rodin-sttt2010.pdf
  42. https://wiki.event-b.org/index.php/Team-based_development
  43. https://prob.hhu.de/
  44. https://link.springer.com/article/10.1007/s10009-007-0063-9
  45. https://prob.hhu.de/w/index.php?title=Event-B
  46. https://wiki.event-b.org/index.php/UML-B
  47. https://eprints.soton.ac.uk/264926/1/SnBu08.pdf
  48. https://wiki.event-b.org/index.php/Event-B_Qualitative_Probability_User_Guide
  49. https://github.com/edwardcrichton/BToolkit
  50. https://ieeexplore.ieee.org/document/1575927/
  51. https://www.atelierb.eu/wp-content/uploads/2023/02/trajectory.pdf
  52. https://www.cambridge.org/core/books/modeling-in-eventb/F39FF5F1B60F0AA585718B8E6A4F9DD7
  53. https://www.researchgate.net/publication/220488203_Model_Checking_Event-B_by_Encoding_into_Alloy
  54. https://inpressco.com/wp-content/uploads/2015/06/Paper1082086-2091.pdf
  55. https://www.ijert.org/research/analysis-of-three-formal-methods-z-b-and-vdm-IJERTV1IS4227.pdf
  56. https://www.overturetool.org/workshops/pre2/Ws2_supporting-co-use-of-VDM-B.pdf
  57. https://www.uml-b.org/
  58. https://www.semanticscholar.org/paper/The-B-book-assigning-programs-to-meanings-Abrial/9162acad763dec8b8b9fee395ffde3fda7247465
  59. https://books.google.com/books/about/Software_Engineering_with_B.html?id=Wy9MAAAAYAAJ
  60. https://dl.acm.org/doi/10.5555/248491
  61. https://www.researchgate.net/publication/343956171_The_First_Twenty-Five_Years_of_Industrial_Use_of_the_B-Method
  62. https://www.event-b.org/abook.html
  63. https://www.bcs.org/media/3093/facts200307.pdf
  64. https://link.springer.com/book/10.1007/978-3-642-11811-1
  65. https://eprints.soton.ac.uk/496103/1/RodinWorkshop2024_proceedings.pdf
  66. https://wiki.event-b.org/index.php/Rodin_Workshop_2025
  67. https://www.systerel.fr/en/expertise/formal-methods/b-method/
  68. https://hal.science/hal-02271391/document
  69. https://www.formalmind.com/blog/if-you-need-comply-iso-26262-iec-61508-or-similar-standards-you-may-need-work-more-formal/
  70. https://ieeexplore.ieee.org/document/7879875
Add your contribution
Related Hubs
User Avatar
No comments yet.