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
Post a Comment