From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.3 required=5.0 tests=BAYES_00,INVALID_MSGID autolearn=no autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,59dddae4a1f01e1a X-Google-Attributes: gid103376,public From: bobduff@world.std.com (Robert A Duff) Subject: Re: Software Safety (was: Need help with PowerPC/Ada and realtime tasking) Date: 1996/05/31 Message-ID: #1/1 X-Deja-AN: 157821989 references: <31AC0712.29DF@lmtas.lmco.com> <31AD794D.2E62@lmtas.lmco.com> organization: The World Public Access UNIX, Brookline, MA newsgroups: comp.lang.ada Date: 1996-05-31T00:00:00+00:00 List-Id: In article <31AD794D.2E62@lmtas.lmco.com>, Ken Garlington 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