Error-free software development for critical systems using the B-Methodology

A description is given of the process of software development for critical systems using the B-Methodology designed by J.R. Abrial. The author explains the insights of the B formal development process: specification and implementation through refinements where each refinement step is proved using axioms based on the first-order predicate logic and an extension of the Zermelo set theory. They present the techniques and related tools that facilitate the process of realizing and proving programs. Three tools are described: the typechecker, the proof-obligation generator and the prover. Two industrial critical software systems have been carried out using this methodology: the subway speed control under final on-site tests (~3000 lines of Modula-2) and the KVS French train speed control that is in the integration test phase (~15000 lines of Ada)