Re: Critique of Ariane 5 paper (finally!)

[dewar@merv.cs.nyu.edu (Robert Dewar)]

Thomas said

<<As an observer to this long-winded thread, can I suggest that you define
what
you mean by reliable? Software engineers such as myself often use the
term
"correctness" to mean what you seem to be talking about above. I would
define "reliability" as the ability of a system to execute correctly
over
some time, and with "normal" inputs ("robustness" would be a measure of
a
system handling pathological inputs). Reliability in my experience has
often been specified by an mtbf - mean time between failures - figure.
So
the aspect of quality we are interested in here is longevity of correct
operation, not just correct function. So, when you say "reliability",
exactly
what do you mean?>>


Sure I think we all accept your definition of reliability (the ability of
a system to execute  correctly ....) although we might want to add something
about ease of modification and maintenance (for me these are also aspects
of reliability).

But that definition is not one we can use directly to ensure reliability.
Sure we can judge in retrospect whether we succeeded in generating a
realiable application, but we can't use this criterion directly to ensure
reliability in advance.

If you look at my earlier postings, you will see that the point you are
making is *precisely* the one that I emaphasized in my replies to Bertrand.

Now what Bertrand claims is that any methodology which results in reliable
programs MUST ALWAYS use an approach that includes an explicit use of DBC.
What I am saying is that there are many methods and techniques that we
use in practice for judging reliability.

Correctness is a different property from reliability as you point out (there
are unreliable correct programs, and reliable incorrect programs). However,
that does not mean that demonstration of correctness is not a useful tool
in the quest after reliability. The effort to demonstrate correctness may
well show up flaws that would indeed effect reliability. Of course even if
you prove total correctness, you have not demonstrated reliability, but then
that is true of other techniques (such as formal testing, etc). In practide,
we ensure reliability by using a variety of techniques and tools.

DBC in the sense in which Bertrand means it is a possible tool. It is
neither necessary nor sufficient, but it is one more useful tool (I cannot
imagine anyone contesting this point). However, use of DBC does not ensure
reliability, and failure to use it does not guarantee unreliability!