[SystemSafety] Bursting the formal methods bubble

[Steve Tockey]

Derek wrote:

³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
their paper:

Analysis of Faults in an N-Version Software Experiment

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING. VOL. 16. NO. 2, FEBRUARY 1990

You can find the paper on line at:

http://sunnyday.mit.edu/papers/nver2.pdf



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
involving boundary value problems) so N-Version development isn¹t really
effective at exposing problems (and is a lot more expensive, at the same
time).


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