[SystemSafety] Bursting the anti formal methods bubble

[Martyn Thomas]

No. Interpret such claims to mean that the part of the code that has
been developed and assured using formal methods is very likely have two
or three orders of magnitude fewer defects than software that has been
developed using typical industrial software development methods. If a
stronger claim is made (such as the claims made by Altran for iFACTS),
then assume the claims are true if they are backed by a guarantee.

Any other claims about "fitness for purpose" should be regarded as
marketing puff unless the developers offer a warranty. This set of
software will include almost every safety-related software-based system,
but the regulators are coming (and civil lawsuits won't be far behind -
see Booker v Toyota).

Martyn



On 25/10/2017 17:08, Derek M Jones wrote:
> can you tell me what the claims about formal methods proving
> correctness actually mean.
>
> Should we interpret these claims to mean:
> "This software is correct, apart from the bugs we have not been able
> to find"? 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20171025/a50c5eb8/attachment-0001.html>