[SystemSafety] Bursting the formal methods bubble

[Steve Tockey]

Derek wrote:

“Using different sets of people increases the probability that problems
will be found in the specification/design, through people having
different points if view and asking different questions (I cannot find a
DOD N-version study that documented this effect).”

I agree that some element of defect identification will happen when more
people are involved, however there are a few points to be made in response:

1) According to the Brilliant, Knight, Leveson paper there won’t be very
much additional defect identification. If I recall correctly, the subjects
in their study were all working to the same requirements specification and
around 60% of the defects they injected were in common to most developers.

2) The cost of building non-trivial software even only once can be pretty
high, building it more than once simply multiplies the cost by the number
of versions built. It can be really, really expensive to build parallel
versions.

3) The same (or higher) defect FINDING effectiveness could easily be
achieved by using an appropriate form of independent peer review, and the
cost of running independent peer reviews on one version being built will
be significantly less than the cost of building N versions.

So I am agreeing that multiple people lead to better work, however all of
the data I have point to the most effective use of most of those people
will be in a peer review capacity not in a build-it-more-than-once
capacity.


― steve



-----Original Message-----
From: systemsafety <systemsafety-bounces at lists.techfak.uni-bielefeld.de>
on behalf of Derek M Jones <derek at knosof.co.uk>
Organization: Knowledge Software, Ltd
Date: Wednesday, October 25, 2017 at 10:57 AM
To: "systemsafety at lists.techfak.uni-bielefeld.de"
<systemsafety at lists.techfak.uni-bielefeld.de>
Subject: Re: [SystemSafety] Bursting the formal methods bubble

Steve,

> ³If you do multiple implementations, e.g., Ada+formal or
> Ada+Visual basic, you will detect more problems and the result will
> be more reliable software.²
> 
> Do you mean ³N-Version development²? If so, this would seem to contradict
> results published by Susan Brilliant, John Knight, and Nancy Leveson in
...
> The point I got out of that paper was that developers don¹t make randomly
> different mistakes, they usually make the same systemic mistakes (notably

People do make the same mistakes, during the specification, design,
requirements and testing phases.

Using different sets of people increases the probability that problems
will be found in the specification/design, through people having
different points if view and asking different questions (I cannot find a
DOD N-version study that documented this effect).

Having multiple implementations provides a means for comparing output,
looking for differences.

There has been some work looking at how using different languages and
computing platforms leads to more 'difference' faults being found.

Would more faults be uncovered by reimplementing an Ada program in
Visual basic or formal methods?  They are both very different.

> -----Original Message-----
> From: systemsafety <systemsafety-bounces at lists.techfak.uni-bielefeld.de>
> on behalf of Derek M Jones <derek at knosof.co.uk>
> Organization: Knowledge Software, Ltd
> Date: Wednesday, October 25, 2017 at 6:36 AM
> To: jean-louis Boulanger <jean.louis.boulanger at gmail.com>
> Cc: "systemsafety at lists.techfak.uni-bielefeld.de"
> <systemsafety at lists.techfak.uni-bielefeld.de>
> Subject: Re: [SystemSafety] Bursting the formal methods bubble
> 
> jean-louis,
> 
>> I thinks that we have more example of mistake in classical development
>> that
>> in formal development
> 
> This is because there is so little formal development, we
> don't have enough data to reliably say one way or the other.
> 
>> yes all method are applied by human and error appear but with formal
>> methods you have a tool to detect it.
> 
> There are tools to detect mistakes in code (not that these are widely
> used :-(
> 
>> with ADA, C .... C++ or JAVA and C# its more difficult to develop a
>> software with a very low level of bug ...
> 
> If you do multiple implementations, e.g., Ada+formal or
> Ada+Visual basic, you will detect more problems and the result will
> be more reliable software.
> 
> The important question is bugs (or lack of) per buck.
> Which technique is the most cost effective?
> 

-- 
Derek M. Jones           Software analysis
tel: +44 (0)1252 520667  blog:shape-of-code.coding-guidelines.com
_______________________________________________
The System Safety Mailing List
systemsafety at TechFak.Uni-Bielefeld.DE