[SystemSafety] Bursting the anti formal methods bubble

[Michael J. Pont]

Peter,

Let me re-phrase my questions (and address them to anyone on this list who cares to express a view).

Suppose Organisation X currently develops software for use in safety-related embedded systems in compliance with one or more international safety standards / guidelines (e.g. IEC 61508, ISO 26262 - or whatever).  

Organisation X does not currently use formal methods / tools.

Organisation X wishes  to improve confidence in the safety of the systems that employ their software.

What level of 'confidence improvement' could Organisation X expect to see through use of tools that allow static analysis of code pre- and post-conditions?   What evidence can be provided to support this?  

[Here I'm assuming something like SPARK or Frama-C tools.] 

What other formal methods / tools could Organisation X consider (if any) if they want to reduce the number of defects in their code by a factor of 100x to 1000x?  What evidence can be provided to support this level of defect reduction (from Organisation X's starting point)?

What level of FM support should Organisation X consider if they want to reduce the threat of civil lawsuits etc (raised in Martyn's original email)?  

---

Some more general comments.

There are people on this list who are formal-method 'fans' (some would say 'fundamentalists').  

In some cases, I think such FM people 'need to get out more' - and spend time with the development teams in real (often fairly small) organisations that are struggling to create safety-related systems.   Such teams usually have very limited time and resources available: this does not mean that they are populated by 'bad people' who want to create poor-quality systems.

Shouting at people because they are not using formal methods doesn't really help ...   Offering suggestions about processes / tools that may help organisations to become 'more formal' would - in my view - be more productive. 

Simply my take (others may well see the world in a different way).

Michael.

---

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