johnson@p.cs.uiuc.edu (03/01/90)
>(T1) Formal proofs of program correctness can provide an absolute, con- >clusive guarantee of program performance; >(T2) Formal proofs of program correctness can provide only relative, in- >conclusive evidence concerning program performance. The problems with these statements is that T1 is not ~T2. NOTHING provides an absolute, conclusive guarentee of program performance. Certainly testing doesn't. However, words like "inconclusive" are loaded with hidden meaning, and I don't want to waste my time doing experiments if I know that they will be inconclusive. I want to conclude something! As a matter of fact, program verification lets you conclude that your program does not have dumb coding errors. Thus, I don't buy either T1 or T2. >(T3) Formal proofs of program correctness should be the exclusive method- >ology for assessing software reliability; >(T4) Formal proofs of program correcness should be the principal method- >ology for assessing software reliability; >(T5) Formal proofs of program correctness should be one among various >methodologies for assessing software reliability. I don't agree with T3, T4, or T5, either. Program verification has nothing to do with assessing software reliability. Program verification make your software more reliable, though, but it doesn't help you measure the reliability, and "assess" means measure to me. "So it becomes a matter of how confident we need to be that a system will perform as it is intended to perform. We cannot know without testing the system." Djikstra: Testing never proves the absence of faults, it only shows their presence. I usually disagree with Djikstra, but this quote of his seems obviously true. However, I will counter with a quote of my own Johnson: If it hasn't been tested then it doesn't work. Specifications need testing more than anything else. Prototyping is a way of testing specifications. Program verification doesn't help specifications very much. Instead, it helps ensure that the code that you produce matches the specification. Thus, testing and verification play complementary roles. However, there are cases where program verification is much better than testing at showing that a system behaves as expected. For example, a couple of years ago there were some people who were killed because an X-ray machine emitted much more power than it should have. The problem was in supposedly in the user interface; the operator missed a decimal point or something and specified too large a number. People claimed that the user interface should have caught this. Maybe, but if I had been building the system and I had been told that NEVER, under ANY circumstances, should the machine emit more than X units of power, then I would have found the one subroutine that turned on power, and written it as EmitPower(power) { if power < X then do lots of low level stuff } Of course, you would have to test that the low level stuff really implemented the high level abstraction. However, after that you would KNOW that the program would never ask for the fatal power. Naturally, if the < operation on the computer breaks, then a patient might still be zapped, but that is a lot less likely than operator mistake. Ralph Johnson -- University of Illinois at Urbana-Champaign
nancy@ics.uci.edu (Nancy Leveson) (03/01/90)
I have been an expert witness in two law suits involving the Therac 25 accident alluded to below. Unfortunately, there is a lot of misinformation about this accident that is circulating. I have figured out how to get around the proprietary information aspects and am preparing a detailed paper that should clear up the misconceptions. Until then, let me just clear up a couple of things to avoid further circulation of misinformation: In article <102100003@p.cs.uiuc.edu> johnson@p.cs.uiuc.edu writes: > >For example, a couple of years ago there were some people who were >killed because an X-ray machine emitted much more power than it >should have. The correct radiation was released, but it was released without the proper filter being in place to reduce the amount of radiation that reached the patient. >The problem was in supposedly in the user interface; This is wrong (along with everything in the article that follows this statement). The problem (actually two problems found so far) was in the code. I think this wrong information originally appeared in an article about this incident that appeared in Datamation, and it has been repeated widely. Although the user interface was far from desirable, it did not cause the accident -- poor programming did. My paper describing the incident details will be available in a month or so, and I will try to get it published quickly -- I have not decided where to send it yet. In the meantime, please be careful when repeating rumors about the Therac accident. So far, everything I have seen written about it has been completely wrong. nancy -- Nancy Leveson
nancy@ics.uci.edu (Nancy Leveson) (03/01/90)
I have been an expert witness in two law suits involving the Therac 25 accident alluded to below. Unfortunately, there is a lot of misinformation about this accident that is circulating. I have figured out how to get around the proprietary information aspects and am preparing a detailed paper that should clear up the misconceptions. Until then, let me just clear up a couple of things to avoid further circulation of misinformation: In article <102100003@p.cs.uiuc.edu> johnson@p.cs.uiuc.edu writes: > >For example, a couple of years ago there were some people who were >killed because an X-ray machine emitted much more power than it >should have. The correct radiation was released, but it was released without the proper filter being in place to reduce the amount of radiation that reached the patient. >The problem was in supposedly in the user interface; This is wrong (along with everything in the article that follows this statement). The problem (actually two problems found so far) was in the code. I think this wrong information originally appeared in an article about this incident that appeared in Datamation, and it has been repeated widely. Although the user interface was far from desirable, it did not cause the accident -- poor programming did. My paper describing the incident details will be available in a month or so, and I will try to get it published quickly -- I have not decided where to send it yet. In the meantime, please be careful when repeating rumors about the Therac accident. So far, everything I have seen written about it has been completely wrong. nancy -- Nancy Leveson