Re: Software Safety (was: Need help with PowerPC/Ada and realtime tasking)

[Ken Garlington <garlingtonke@lmtas.lmco.com>]

Robert A Duff wrote:
> 
> The problem is that, in English, "correct" is an absolute term.  If you
> say "This flight-control software has been mathematically proven to be
> correct", there's a danger that non-programmers will believe, "They've
> proven (beyond any doubt) that the software will do what it ought to do"
> (i.e. the non-programmer misses the point that "what it ought to do" is
> not necessarily the same thing as what the formal spec said).

True - which is why, if anyone were to say to me that their software was
"proven" to be "correct", I would consider them poor engineers if they
didn't also define their terms. (Personally, I don't believe it is possible
to "prove" flight control software even matches the spec. It is only possible
to reason about the spec mathemetically, and build some level of confidence
in its correctness.)

> Using the term "correct" as the proof-of-correctness folks like to,
> gives a false sense of security, IMHO.  *My* meaning for "correct" is
> harder to deal with, of course, because it requires human judgement
> (what the program *ought* to do, as opposed to what somebody formally
> *specified* it should do).  Well, that's life.

It also means that your definition of "correct" may not be desirable as
the basis for releasing flight control software to the field. Usually,
we want something more concrete than "it feels right." (Of course, it's
perfectly OK for the _developer_ to use an intuitive notion of "correct"
as one of the criteria :)

-- 
LMTAS - "Our Brand Means Quality"