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

[bobduff@world.std.com (Robert A Duff)]

In article <31AD794D.2E62@lmtas.lmco.com>,
Ken Garlington  <garlingtonke@lmtas.lmco.com> wrote:
>I have some sympathy for your more general definition, but there's also a
>problem. For example, I cannot build a flight-control system that will
>prevent aircraft crashes. No matter what I do, there will always be some
>chain of events (plausible or otherwise) that will cause the plane to
>crash. On an F-16, it's as simple as the pilot pointing the nose to the
>ground too long, or flying through a sufficiently strong hurricane. Does
>this make flight-control software inherently incorrect, or just inherently
>unsafe under certain conditions?

Agreed.  We don't know for sure if that crash was the fault of the
software or the pilot.  We can study the circumstances, and come to an
opinion, but intelligent people will disagree on the point.

My objection to using the word "correct" to mean "software conforms to
some (possibly bogus) formal spec", is that it *automatically* blames
the pilot, even in cases where intelligent people would blame the
software.  Suppose the software gave confusing info to the pilot.  I
don't want some programmer saying, "But, the formal spec *required* the
software to give that confusing info, and we used formal correctness
proofs to ensure that."

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

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.

>Any requirements specification, formal or otherwise, has to make some
>assumptions about the operating environment, and it has to make some
>assumptions about "acceptable" chains of events that lead to unsafe
>conditions. A requirements specification for a robot control arm may
>assume that no humans will be in the vicinity during operation. This
>may be a reasonable assumption, given the planned operating environment.
>If a human is standing next to the arm during operation, and the arm
>starts moving without warning and hits the human, was the software incorrect?
>Was it unsafe? In this case, even with a general definition of "correctness",
>the software might very well be considered correct, but unsafe (did not have
>a warning function).

Was it unsafe?  I don't know.  It requires some human beings who know
about the situation to judge whether it was reasonable to assume that
the robot is out of reach of humans.  No mathematical proof techniques
are going to help you, there.  I think that if you mathematically prove
that program X obeys formal spec Y, then you should say, "I proved X
obeys Y", and not "I proved X is correct".  Even "I proved X correct
with respect to Y" is subject to misinterpretation, and the false sense
of security (which might lead to the robot boss telling a person to go
over there near the robot and...).

>Note that the reverse is also possible. If the software was supposed to
>command the robot arm to move, and it fails to do so, this might very
>well be incorrect, but safe.

Agreed.

- Bob