[SystemSafety] Bursting the anti formal methods bubble

[Michael J. Pont]

Peter,

These comments are useful - thank you.

Michael.

-----Original Message-----
From: systemsafety [mailto:systemsafety-bounces at lists.techfak.uni-bielefeld.de] On Behalf Of Peter Bernard Ladkin
Sent: 26 October 2017 12:59
To: systemsafety at lists.techfak.uni-bielefeld.de
Subject: Re: [SystemSafety] Bursting the anti formal methods bubble

On 2017-10-26 11:21 , Michael J. Pont wrote:
> Suppose Organisation X currently develops software .......
> 
> What level of 'confidence improvement' could Organisation X expect to see through use of tools ....

I find your question much too general to be able to hazard a single meaningful answer.
Compare:
* Suppose organisation X.....
* Organisation X does not currently use Ada....
* Organisation X wishes .....
* What level of "confidence improvement" could Organisation X expect to see through use of the Ravenscar profile? Etc....

It depends on the organisation; it depends on what their current practices are; it depends on the skill and intellectual competence of its staff in using and integrating technology new to it; it depends if they have anyone on board who *really knows* Ada and Ravenscar, as well as the application domain; and so on. Barry Boehm & co have a lengthy and very involved book about estimating SW development steps with COCOMO II (his Contributory Cost Model, updated from the SEE
version) and even for those straightforward steps there are a lot of individual data about demonstrated company capabilities required.

It becomes easier to answer your question if it is specialised to specific properties of delivered code:
* What level of "confidence improvement" in absence of buffer-overflow vulnerabilities in its code could Organisation X expect if it switches to using a language with strong typing?
* Answer: complete confidence in their absence.

The setup of your question is also a bit odd: Organisation X cannot be building any components with SIL 3 and SIL 4 requirements. And if they are not competent to do that, I wonder who would have confidence in their ability to build SIL 1 or SIL 2 components? If you are a big systems integrator, wouldn't you rather use a company which can do it all? I'm thinking of a specific company which builds reliable SW-driven thermometers for process-plant use. They don't sell their stuff as SIL 1/2-capable, because few would buy them if that is all they were. People want allegedly SIL 3/4-capable kit, even if the actual requirement is only SIL 1 or SIL 2, because they want the assurance of highest reliability. So their SIL 3/4-capable kit is what sells.

> 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)?

There are hundreds of mathematical methods out there which could theoretically improve the quality of code. Are you really asking for a list? How would anyone know whether Method Y would improve Organisation X's defect density by a given amount in advance of trying it and seeing?

> 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)?  

I don't know what counts as a "level of FM support". Neither do I know much about the "threat of civil lawsuits". Organisation X should use best practice as a matter of general legal obligation, and if there is something bad which they could have avoided through use of best practice then they could get hung in some court. If a SIL 3 component goes wonky, kills someone, and Organisation X didn't make reasonable use of FM in its development, I would like to think there is a good chance that HSE will prosecute them in criminal court, because that is what they said they do.

> 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.  

That is an ad-hominem argument which I reject as such. Sure there are people who advocate FM who have no real clue how to build SW that runs in real products. So what? There are all sorts of people on the face of this earth.

Or I could counter it. A decade and a half ago, the world's most successful signalling system provider had a neat system. They configured a new signalling system for, say, a large railway station (let's say 15-20 platforms plus sidings) on a model. Then they went through a series of automated steps to get the configuration code for the switches, in Pascal (as I remember). Then, the Pascal was reverse-engineered back into the modelling language and they ran the reverse-engineered model against the original model to make sure they were the same. And this was signed off by the local-country regulator as an approved method for configuring signalling systems.

Do I know people in "fairly small organisations struggling..." who could do that? Not very many.
Some. But that was the competition fifteen years ago if you were doing railway signalling. Why did the big company do it this way? Because it was more efficient, more reliable and made them more money, or some combination of those, I presume. That would be the same reason Airbus uses Lustre to design state machines for some DAL A systems, then presses a few buttons in their SCADE toolset to get the object code out the back. Who could possibly object to such technology, and why?

(You'll notice from Rod's post, and here, that if you take a bunch of FMs and offer them joined-up in a package, you can call it a toolset or a toolsuite, and also a (singular) FM.)

> Shouting at people because they are not using formal methods doesn't really help ...   
> 
> Simply my take (others may well see the world in a different way).

I think shouting at people because they are not using formal methods is quite appropriate behaviour for a regulator, or an assessor, if they are building it to IEC 61508-3:2010 SIL 3, for example.

PBL

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