Error-free software development for critical systems using the B-Methodology
The work
| Authors | M. Carnot; Clara DaSilva; Babak Dehbonei; Fernando Mejia |
|---|---|
| Editors | |
| Type | misc |
| Year | 2003 |
| Citekey | carnot2003errorfree |
Where it appeared
| Published in | Proceedings/Proceedings - International Symposium on Software Reliability Engineering |
|---|---|
| Publisher | Institute of Electrical and Electronics Engineers |
| Volume | 11 |
| Pages | 274--281 |
Identifiers
| DOI | 10.1109/issre.1992.285893 |
|---|---|
| OpenAlex | W2132084411 |
Access
| Landing page | https://doi.org/10.1109/issre.1992.285893 |
|---|
From OpenAlex, which stores abstracts as an index of words and their positions: what is shown is rebuilt from that, and reads fluently whether or not it is what the author wrote.
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).>
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-10-23 19:52 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Cite it as
@misc{carnot2003errorfree,
title = {Error-free software development for critical systems using the B-Methodology},
author = {M. Carnot and Clara DaSilva and Babak Dehbonei and Fernando Mejia},
year = {2003},
journal = {Proceedings/Proceedings - International Symposium on Software Reliability Engineering},
publisher = {Institute of Electrical and Electronics Engineers},
volume = {11},
pages = {274--281},
doi = {10.1109/issre.1992.285893},
}
This record lives at https://refs.drheap.org/carnot2003errorfree/ and will keep doing so.