[SystemSafety] Bursting the anti formal methods bubble

[Peter Bernard Ladkin]

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





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