Abstract | ||
---|---|---|
Software is becoming increasingly involved in safety-critical systems. Such systems are ideal fields of application of formal methods. A rigorous development accompanied by formal proofs is a guarantee of the correctness of the development. We summarize our experience of using the B formal method in the development of safety-critical railway signalling applications. Our applications range in size from 2000 lines to 22000 lines. They are specified, refined and implemented in B. Issues (technical and non technical) related to the utilization of B are discussed and solutions presented. |
Year | DOI | Venue |
---|---|---|
1994 | 10.1007/3-540-58555-9_84 | FME |
Keywords | Field | DocType |
railways signalling industry,formal methods,formal method | Signalling,Software engineering,Control flow graph,Computer science,Correctness,Theoretical computer science,Mathematical proof,Software,Formal methods,Proof obligation,Railway signalling | Conference |
ISBN | Citations | PageRank |
3-540-58555-9 | 12 | 0.98 |
References | Authors | |
2 | 2 |
Name | Order | Citations | PageRank |
---|---|---|---|
Babak Dehbonei | 1 | 65 | 9.68 |
Fernando Mejia | 2 | 34 | 5.11 |