B, the language created by Jean-Raymond Abrial [1], stands (as a “confidential informant” had revealed to me more than a decade ago) for “Bourbaki.” The letter refers to a 19th-century French general of Greek descent, Nicolas Bourbaki, whose name was adopted in the 1930s as a single, collective pseudonym by a group of French mathematicians seeking to reconstruct all of mathematics with full rigor, from the ground up. “Nicolas Bourbaki” soon included prominent non-French mathematicians, and “his” mathematical volumes, highly formal in “the Bourbaki style,” continue to be well known [2], if not to everyone’s taste [3]. (This matter of taste is not relevant to the B-based formal-methods tools that are expounded in the excellent book under review, though no application of the contemporary formal-methods languages comprising today’s Tower of Babel is the proverbial “walk in the park.”)

Abrial’s B is not to be confused with the B of BCPL, the precursor to Dennis Ritchie’s sensational and now-ubiquitous C, arguably the preeminent procedural programming language that is per se completely devoid of problem-domain specification or verification semantics. (I hasten to add that extra language facilities can be, and have substantially been, added via C libraries or “literate programming” [4] infrastructure.) Abrial also had, prior to (his) B, a hand (or two) in the design and implementation of the Z specification language [5], which is named for Zermelo-Fraenkel (of axiomatic set-theory fame [6]). Set theory is, in addition to first-order logic, a pillar of this B.

The formal methods (FMs) level of abstraction is higher than that of B. Formal methods address what is arguably the most serious issue associated with the design of computer-driven systems and software, namely, correctness, which cannot be adequately “tested into” even systems of moderate size. The only recourse is mathematical proofs (of safety and security properties, and so on), be they syntactic (theorem-proving, as is B) or semantic (model-checking, as are SAT-solver-based tools [7]).

Here are the chapter titles and page counts:

1. “Presentation of the B-Method” (34 pages)

2. “Atelier B” (12 pages)

3. “B Tools” (36 pages)

4. “The B Method at Siemens” (46 pages)

5. “Industrial Applications for Modeling with the B Method” (22 pages)

6. “Formalization of Digital Circuits Using the B Method” (36 pages)

7. “Pragmatic Use of B: The Power of Formal Methods without the Bulk” (14 pages)

8. “BRILLIANT/BCaml – A Free Tools Platform for the B Method” (10 pages)

9. “Translating B and Event-B Machines to Java and JML” (42 pages)

10. “Event B” (46 pages)

11. “B-RAIL: UML to B Transformation in Modeling a Level Crossing” (50 pages)

12. “Feasibility of the Use of Formal Methods for Manufacturing Systems” (42 pages)

13. “B Extended to Floating-Point Numbers: Is It Sufficient for Proving Avionics Software?” (36 pages)

14. “From Animation to Data Validation: The ProB Constraint Solver 10 Years On” (20 pages)

15. “Unified Train Driving Policy” (28 pages)

16. “Conclusion” (6 pages)

Correctness of safety-critical systems, my own venue for the last 16 years and counting, mandates nothing less than proof that the design entails invariable preservation of the operational system’s behavioral safety properties, and I have managed the application of the B-method and of (event-driven) System-B throughout those system life cycles.

This 27-author volume (its editor doubling as an author) is excellent in all aspects: production quality; reasonable flow, considering its full spectrum of B-related topics; authority of its expert authors; uniformity in good writing; and apposite and clear code and diagrammatic examples and illustrations. The book is an ostensive demonstration that at least this formal method, that is B, has broad and ever-growing applications. The book has answered questions that I have asked for the last two decades, and some that I’ve not asked. Among the former is the floating-point issue (chapter 13), a bugaboo spanning all of computing, formal or not. Among the latter is synthesis of B with such functional programming languages as OCaml (chapter 8).

This excellent book is not to be missed by anyone seriously involved in high-assurance design. I look forward to reading others in its series.