[SystemSafety] Bursting the anti formal methods bubble

[Michael J. Pont]

Martyn,

 

You make a number of strong claims here, and I have some questions.

 

What is your baseline - what do you mean by “typical industrial software methods”?  Do you – for example - mean products developed in compliance with IEC 61508 (e.g. ‘SIL 3’)?  ISO 26262 (e.g. ‘ASIL D’)?

 

What do you mean by FMs?   Would use of SPARK Pro qualify?  Use of Frama-C?  Something else?

 

If you can provide evidence that use of a specific FM is capable of providing “two or three orders of magnitude fewer defects” in an IEC 61508 / ISO 26262 project, I’d be interested to see this.

 

Michael.

---

On 25/10/2017 17:39, Martyn Thomas wrote:

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/20171026/1c055d94/attachment.html>