[SystemSafety] Correctness by Construction

[Dewi Daniels]

On Mon, 13 Jul 2020 at 19:29, <andrew at andrewbanks.com> wrote:

> But surely, at some stage, "Correctness" can only be actually proven by
> EXECUTING that code on the target hardware.
>
> There are nuances and subtleties that can only ever be truly discovered
> by running the code it its true environment.


As far as I know, the proponents of “Correctness by Construction” have
never claimed that testing has no role to play in software verification.
Rather, it is their contention that other techniques, including formal
methods but also including methods such as critical inspection of one’s own
code, are more efficient and more effective in demonstrating certain
properties of the software.

I’m reminded of an anecdote in the “The Machine That Changed The World”,
the book about lean production. At the time the book was written (1991),
the only difference between the Volkswagen production line and the
Mercedes-Benz production line was that Mercedes-Benz employed technicians
to check each car that came off the production line and fix any defects
found. That was why Mercedes-Benz cars were higher quality, but also more
expensive, than Volkswagens. On the other hand, Toyota stopped the
production line as soon as any component was found to be out of tolerance.
They carried out root-cause analysis so as to eliminate the defect at
source. Toyota claimed that the production line soon settled down to
produce cars in which every component worked as intended, meaning they
could manufacture cars with the quality of a Mercedes-Benz for the price of
a Volkswagen,

Yours,
Dewi

> --

Yours,

Dewi Daniels | Director | Software Safety Limited

Telephone +44 7968 837742 | Email d <ddaniels at verocel.com>
ewi.daniels at software-safety.com

Software Safety Limited is a company registered in England and Wales.
Company number: 9390590. Registered office: Fairfield, 30F Bratton Road,
West Ashton, Trowbridge, United Kingdom BA14 6AZ
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/pipermail/systemsafety/attachments/20200713/f7635361/attachment.html>