RE: Bug-free software (was: Re rant about virii on VMS...)

["David Crocker" <dcrocker () eschertech com>]

"der Mouse" wrote:

> >
Any nontrivial piece of software has bugs.
<<

No, there are some nontrivial pieces of software in which bugs have never been
found and there is no reason to believe any exist. I'm thinking here of
safety-critical software developed using formal specification, verified
refinement and automatic code generation, such as the METEOR system that
controls driverless trains on the Paris metro. To quote from the paper by
Patrick Cousot and Radhia Cousot:

"The 115 000 lines specification written in B compiles into a 87 000 lines ADA
program. ... Since the metro is running, no error was ever claimed to be found
in the embedded software nor in its B specification. Indeed all errors, if any,
could only be found at the interfaces, the specification of which might not have
been satisfied by the central control software (not developped in B and itself
potentially subject to errors). One may wonder why, after such a successful
experience, theoremproving based formal methods are not standard for the design
of safety critical embedded software."

David Crocker
Escher Technologies Ltd.
www.eschertech.com
Tel. +44(0)1252 336565  Fax +44(0)1252 320954