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

 https://ieeexplore.ieee.org/document/285893

Abstract:

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 ( approximately 3000 lines of Modula-2) and the KVS French train speed control that is in the integration test phase ( approximately 15000 lines of Ada).
 
Date of Conference: 07-10 October 1992
Date Added to IEEE Xplore: 06 August 2002
Print ISBN:0-8186-2975-4
Conference Location: Research Triangle Park, NC, USA
 

Comments

Popular posts from this blog

Ce que je dois à Jean-Raymond Abrial

Jean-Raymond Abrial (1938, 2025)

On B, Jean-Raymond Abrial