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: Ken Garlington Subject: Software Safety (was: Need help with PowerPC/Ada and realtime tasking) Date: 1996/05/30 Message-ID: <31AD794D.2E62@lmtas.lmco.com>#1/1 X-Deja-AN: 157568767 references: <63085717wnr@diphi.demon.co.uk> <31AC0712.29DF@lmtas.lmco.com> content-type: text/plain; charset=us-ascii organization: Lockheed Martin Tactical Aircraft Systems mime-version: 1.0 newsgroups: comp.lang.ada x-mailer: Mozilla 2.01 (Macintosh; I; 68K) Date: 1996-05-30T00:00:00+00:00 List-Id: Robert A Duff wrote: > > In article <31AC0712.29DF@lmtas.lmco.com>, > Ken Garlington wrote: > > >It sounds like the point has already been made, but it is also good to > >remmeber that, technically, correctness and safety don't have to be related. > >You can have correct software that is unsafe, and incorrect software that > >is safe. > > I suppose it depends on your definition of "correct". The > proof-of-correctness folks define "correct" to mean "correctly obeys the > formal specification". To me, that's a bogus definition. In plain > English, a "correct" program is one that does what it's supposed to do, > regardless of whether the specification is wrong. If you show me a word > processor that deletes my file when I told it to italicize a word, to > me, that's incorrect, even if you can show me a (bogus) formal spec that > says that the "italicize word" function should delete files. If you > show me a flight-control program that crashes airplanes, that's > incorrect IMHO, despite the fact that you might show me a formal spec > saying it did what the formal spec says. 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? 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). 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. -- LMTAS - "Our Brand Means Quality"