[SystemSafety] Bursting the formal methods bubble

[Derek M Jones]

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