[SystemSafety] Bursting the anti formal methods bubble

Peter Bernard Ladkin ladkin at rvs.uni-bielefeld.de
Thu Oct 26 09:40:11 CEST 2017


Michael,

On 2017-10-26 09:05 , Michael J. Pont wrote:
> 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’)?

In https://www-users.cs.york.ac.uk/tpk/nucfuture.pdf , John McD and Tim Kelly talk about typical
fault densities. They suggest that 1 error per KLOC is considered to be "world-class" for some areas
of safety-critical systems. The C130J software had about 23 errors per KLOC and 1.4 safety-critical
errors per KLOC.

In contrast, Praxis, now Altran UK, has instrumented its code quality for a long time and has
achieved fault densities as low as 1 per 25KLOC.

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

The answer is trivially no, because you are asking about apples and your examples are oranges.

SPARK Pro and Frama-C are PDEs. A FM is first and foremost a method. Both SPARK Pro and Frama-C use
FMs, for example SPARK Pro uses Bergeretti-Carre information flow analysis integrally.  The SPARK
Examiner uses Hoare Logic for static analysis, as well as other methods.

> 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.
That is a different ask from what Martyn said. Also, in a safety-critical context just using one FM
is not going to get you very far. Using Z to write your requirements specifications, for example,
isn't going to get you very far if you then simply give your Z requirements to designers who can't
read Z. You need more stuff to support that one technique, and you need your techniques to be joined up.

But I can give you some obvious examples from the past. First, use of strong typing would have
eliminated 80% of the networked-SW vulnerabilities listed by US CERT in the 1990's. Strong data
typing is an FM introduced 49 years ago. Second, use of higher-level languages and their compilers
led to much more reliable code than writing it all in assembler. HLL Compilers are FM (if you are
surprised by that assertion, a quick revisit of Aho, Hopcroft and Ullmann will make it clear).

PBL

Prof. Peter Bernard Ladkin, Bielefeld, Germany
MoreInCommon
Je suis Charlie
Tel+msg +49 (0)521 880 7319  www.rvs-bi.de





-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 525 bytes
Desc: OpenPGP digital signature
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20171026/300b0cbe/attachment.sig>


More information about the systemsafety mailing list