Name
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 (~3000 lines of Modula-2) and the KVS French train speed control that is in the integration test phase (~15000 lines of Ada) |
Year | DOI | Venue |
|---|---|---|
1992 | 10.1109/ISSRE.1992.285893 | International Symposium on Software Reliability Engineering |
Keywords | Field | DocType |
formal logic,formal specification,set theory,software reliability,theorem proving,Ada,B formal development process,B-Methodology,KVS French train speed control,Modula-2,Zermelo set theory,critical systems,first-order predicate logic,industrial critical software systems,integration test phase,proof-obligation generator,prover,refinement step,software development,specification,subway speed control,typechecker | Programming language,Integration testing,Software engineering,Computer science,Automated theorem proving,Software system,Formal specification,Software quality,Gas meter prover,Predicate logic,Software development,Reliability engineering | Conference |
Citations | PageRank | References |
11 | 3.03 | 6 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Michel Carnot | 1 | 11 | 3.03 |
| Clara DaSilva | 2 | 11 | 3.03 |
| Babak Dehbonei | 3 | 65 | 9.68 |
| Fernando Mejia | 4 | 34 | 5.11 |