[SystemSafety] Bursting the formal methods bubble

[Derek M Jones]

Steve,

> “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).”

It was a NASA study, see table 4-1:
https://ntrs.nasa.gov/search.jsp?R=19870020663

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

Is the problem size an issue?  The Brilliant et al study required a mean
effort of 47 hours to complete, the NASA study hired everybody for 10 weeks.

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

Yes, this is one reason why formal methods (which essentially creates
a whole new implementation) is only used for critical cases.

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

Do you have any data on this?

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

This is one argument.  The whole issue is being discussed in a ultra-low
data environment (there are small specific bits and pieces floating
around).

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