136
Proofs, Induction, and Number Theory
speCial interest page
Making Safer Software
Proof of correctness seeks to verify that a given computer program or segment of a program meets its specifications. As we have seen, this approach relies on
formal logic to prove that if a certain relationship (the
precondition) holds among the program variables before
a given statement is executed, then after execution another relationship (the postcondition) holds. Because of
the labor-intensive nature of proof of correctness, its use
is typically reserved for critical sections of code in important applications.
The B method is a set of tools that does two things:
1. Supports formal project specification by means
of an abstract model of the system to be developed. This support includes both automatic generation of lemmas that must be proven in order
to guarantee that the model reflects the system
requirements and automatic proof tools to prove
each lemma or flag it for human verification
assistance.
2. Translates the abstract model into a code-ready
design, again using lemmas to ensure that the
design matches the abstract model. The final
level can then be translated into code, often using the Ada programming language, described
by its proponents as “the language designed for
building systems that really matter.”
One of the most interesting applications of proof
of correctness, based on the B method, is the development of software for the Paris Météor train. This is part
of the Paris metro train system designed to carry up to
40,000 passengers per hour and per direction with an
interval between trains as low as 85 seconds on peak
hours. The safety-critical part of the software includes
the running and stopping of every train, opening and
closing of doors, electrical traction power, routes,
speed of trains, and alarms from passengers. By the
end of the project, 27,800 lemmas had been proven,
with 92% proven automatically (with no human intervention). But here is the amazing part: the number of
bugs in the Ada code found by testing on the host computer, the target computer, on site, and after the system
was put into operation was—0. Zero, nada, none. Very
impressive indeed.
Other formal method systems have been used for
critical software projects, such as
• Development of a left ventricular assist device
that helps the heart pump blood in those with
congestive heart failure. The eventual goal is an
artificial heart.
• “Conflict detection and resolution algorithms”
for safety in air traffic control
• Development of the Tokeneer ID Station software to perform biometric verification of a human seeking access to a secure computing environment. Tokeneer is a hypothetical system
promoted by NSA (National Security Agency) as
a challenge problem for security researchers.
Formal Verification of Large Software Systems, Yin, X.,
and Knight, J., Proceedings of the NASA Formal
Methods Symposium, April 13–15, 2010, Washington
D.C., USA.
http://libre.adacore.com/academia/projects-single/echo
http://shemesh.larc.nasa.gov/fm/fm-atm-cdr.html
“Météor: A Successful Application of B in a Large Project,”
Behm, P., Benoit, P., Faivre, A., and Meynadier, J.,
World Congress On Formal Methods in the Development of Computing Systems, Toulouse, France, 1999,
vol. 1709, pp. 369–387.
C h a p t e r
2 2
Proofs, Induction, and Number Theory
speCial interest page
Making Safer Software
Proof of correctness seeks to verify that a given computer program or segment of a program meets its specifications. As we have seen, this approach relies on
formal logic to prove that if a certain relationship (the
precondition) holds among the program variables before
a given statement is executed, then after execution another relationship (the postcondition) holds. Because of
the labor-intensive nature of proof of correctness, its use
is typically reserved for critical sections of code in important applications.
The B method is a set of tools that does two things:
1. Supports formal project specification by means
of an abstract model of the system to be developed. This support includes both automatic generation of lemmas that must be proven in order
to guarantee that the model reflects the system
requirements and automatic proof tools to prove
each lemma or flag it for human verification
assistance.
2. Translates the abstract model into a code-ready
design, again using lemmas to ensure that the
design matches the abstract model. The final
level can then be translated into code, often using the Ada programming language, described
by its proponents as “the language designed for
building systems that really matter.”
One of the most interesting applications of proof
of correctness, based on the B method, is the development of software for the Paris Météor train. This is part
of the Paris metro train system designed to carry up to
40,000 passengers per hour and per direction with an
interval between trains as low as 85 seconds on peak
hours. The safety-critical part of the software includes
the running and stopping of every train, opening and
closing of doors, electrical traction power, routes,
speed of trains, and alarms from passengers. By the
end of the project, 27,800 lemmas had been proven,
with 92% proven automatically (with no human intervention). But here is the amazing part: the number of
bugs in the Ada code found by testing on the host computer, the target computer, on site, and after the system
was put into operation was—0. Zero, nada, none. Very
impressive indeed.
Other formal method systems have been used for
critical software projects, such as
• Development of a left ventricular assist device
that helps the heart pump blood in those with
congestive heart failure. The eventual goal is an
artificial heart.
• “Conflict detection and resolution algorithms”
for safety in air traffic control
• Development of the Tokeneer ID Station software to perform biometric verification of a human seeking access to a secure computing environment. Tokeneer is a hypothetical system
promoted by NSA (National Security Agency) as
a challenge problem for security researchers.
Formal Verification of Large Software Systems, Yin, X.,
and Knight, J., Proceedings of the NASA Formal
Methods Symposium, April 13–15, 2010, Washington
D.C., USA.
http://libre.adacore.com/academia/projects-single/echo
http://shemesh.larc.nasa.gov/fm/fm-atm-cdr.html
“Météor: A Successful Application of B in a Large Project,”
Behm, P., Benoit, P., Faivre, A., and Meynadier, J.,
World Congress On Formal Methods in the Development of Computing Systems, Toulouse, France, 1999,
vol. 1709, pp. 369–387.
C h a p t e r
2 2