RISKS-LIST: RISKS-FORUM Digest Monday 22 May 1989 Volume 8 : Issue 73 FORUM ON RISKS TO THE PUBLIC IN COMPUTERS AND RELATED SYSTEMS ACM Committee on Computers and Public Policy, Peter G. Neumann, moderator Contents: State computer system scrapped (Bruce Forstall) Fax Attack (Chuck Dunlop) Client responsibility for organization's head crash (David A Honig) Re: Computers in mathematical proofs (Robert Lee Wilson Jr, Robert English, Travis Lee Winfrey) Formal Methods -- Call For Papers (Nancy Leveson) *** My access has been very restricted & time limited. With GREAT PAINS, *** *** RISKS-8.72 was EMACSed blind through a nonemulating screen interface. *** *** ABOVE AND BEYOND the call of duty. Backlog still large. Sorry. PGN *** ---------------------------------------------------------------------- Date: Mon, 22 May 89 12:20:11 PDT From: forstall@june.cs.washington.edu (Bruce Forstall) Subject: State computer system scrapped (Reprinted WITH permission of The Seattle Times, Friday, May 19, 1989, p. B1) State bytes off more than it can chew DSHS to scrap computer system by Jim Simon, Times Olympia bureau OLYMPIA -- After the state spent $20 million and nearly seven years trying to computerize its public-assistance program, the first caseworkers to use the so-called COSMOS system made their own discovery: They could figure out a client's benefits faster by hand than with the computer. The Department of Social and Health Services announced yesterday it was swallowing its losses and terminating COSMOS, considered the most expensive, and some say ill-advised, computerization effort ever undertaken by the state. ``The project needed to be stopped and we stopped COSMOS,'' said DSHS Secretary Richard Thompson, the fifth agency head who has wrestled with the system. ``There's a lot of things that went wrong that we still have to look at. My concern was that we had to stop spending the money.'' The state has so far spent about $4.1 million and federal agencies about $15.2 million on COSMOS--the Community Services Management and Operations System. Thompson said DSHS ultimately may be liable for up to $4 million of the federal share. A consultant's report released earlier this week recommended scuttling COSMOS. The report cited poor management, an overly complex design, difficulty to use by caseworkers and the use of untested software. Proponents originally predicted the troubled system would save the state money by allowing computers rather than caseworkers to calculate eligibility for welfare, food stamps and medical assistance. COSMOS, designed by Pennsylvania-based UNISYS Corp., was thought so advanced that Gov. Booth Gardner and some of the state's computer professionals likened it to ``artificial intelligence.'' But its complexity apparently kept it from working at all. That became obvious this year when the system was installed on a pilot basis in the Longview and Vancouver DSHS offices, according to Thompson and others. Workers there found it took up to twice as long to figure out a client's eligibility from COSMOS as it did manually. Using the computer resulted in frequent errors in simple calculations, and perhaps most nerve-wracking for caseworkers, the screen often went blank for long intervals. ``This was an effort to create artificial intelligence so the computer could `think' about eligibility,'' Gardner said yesterday. ``I don't think we'll mess with artificial intelligence again.'' But critics say DSHS had plenty of advance warning about just how high a risk COSMOS represented. In 1982, when planning first began, the agency estimated it would cost $10 million and be completed in 1985. But the agency later sought a more ambitious system that was to cost $22 million and be completed by the end of mid-1987. Before killing COSMOS, the most recent estimates were that it would cost $38 million and take until late 1990 to finish. Gerald Reilly, who headed the DSHS division of income assistance until recently, said the agency decided to keep pressing on until they could test COSMOS in the field. ``We believed you couldn't know how this would work until you took it that far,'' Reilly said. Reilly and others acknowledge that the state was aware of problems UNISYS had setting up similar systems for other states. ``But virtually all these big systems have troubles,'' Reilly said. ``The welfare programs themselves are very complex.'' ``Killing COSMOS was a gutsy move by Thompson,'' said Rep. Gary Locke, chairman of the House Appropriations Committee. ``There's going to be a lot of finger-pointing but there was no sense chasing the good money after the bad.'' The death of COSMOS could prove an embarrassment for UNISYS, which has already been paid about $4.7 million. Two sources said the state attorney general's office is considering legal action. The attorney general's office declined to comment. A spokesman for UNISYS' local office also would not comment. Thompson said the agency will still pursue a system to computerize its benefit programs. But the next effort will probably use one of the 17 systems certified by the federal government using technology that has been tested in other states, he said. Another major state computer project that has cost taxpayers $17 million is expected to be scrapped next year. State officials have said they expect to cancel the project to transfer district-court records because it doesn't perform anywhere near the number of tasks court officials expected it would. ------------------------------ Date: Sat, 13 May 89 12:29:28 EDT From: Chuck_Dunlop@ub.cc.umich.edu Subject: Fax Attack Governor's try to ban unsolicited ads backfires (The Ann Arbor News, 5/13/89) HARTFORD, Conn - The great fax attack of 1989 -- an all-out lobbying campaign against a bill banning unsolicited facsimile advertising -- may have backfired when the governor's fax machine was jammed for hours with unwanted messages. Starting Thursday and continuing Friday, Gov. William A. O'Neill's fax machine has been beeping constantly, spitting out unwanted messages from angry businesses that advertise by fax. The businesses oppose a bill now awaiting O'Neill's signature that would prohibit them from marketing their products by fax without first obtaining the permission of the recipient. Violators would face a $200 fine. Starting Thursday morning, dozens of Connecticut businesses faxed to O'Neill's office a form letter arguing against the fax ban. The stream of fax messages was so constant -- 40 came in before 10 a.m. -- that the governor's office turned off the fax machine Thursday. O'Neill's press secretary, Jon. L. Sandberg, said the governor still hasn't decided whether he will sign the bill. But aides to the governor said the persistent lobbying campaign proved how annoying unwanted messages casn be. The inconvenience was compounded because the governor's office was unable to use its fax machine to receive information about spring flooding around the state. ------------------------------ Date: Wed, 17 May 89 09:22:49 -0700 From: David A Honig Subject: Client responsibility for organization's head crash I recently was sent a bill ($70) for two "lost books" from the campus's (U.C. Irvine) main library. Since I knew I had returned them, I went to check the shelves. I found one of them; I didn't have time to search for the other. When I inquired as to why I had been falsely charged and billed, I was told by the checkout clerk that it was a "computer error". Upon phoning the library, I found that the day I had returned the books the library had had a head crash. The library policy is to search for "lost" books if the charge is contested, but if they are not found, I am assumed guilty. (What if the reshelvers erred?) There is essentially no recourse; I understand that the Ombudsman would be impotent. Worse, I am told that this occurs occasionally to others, head crash or not. What I find remarkable is that this organization would not give the client the benefit of the doubt when they are *aware of an internal problem*. Besides this, I wonder about the tradeoffs they made in designing a book-return system so vulnerable to the failure of one of its components (disk drive or human book checker). Are redundant drives or paper records so expensive that a major library cannot use them? I suspect the adminstrators who specified the existing system did not understand what they were doing. I suppose I should not be surprised. ------------------------------ Date: Tue, 16 May 89 10:24:27 PDT From: bobw@ford-wdl44 (Robert Lee Wilson Jr) Subject: Re: Computers in mathematical proofs While "dying off" of some of the mathematicians who found the computerized 4-color proof intolerable is certainly part of the reason that the computerized "no projective plane of order 10" proof is being accepted, I think there is another significant difference. I knew several mathematicians who had "gone out on a limb" with statements that 4 colors would not suffice, no matter what the predominant belief. I can recall one whose entire career and psyche were devoted to finding non-4-colorable maps. He would literally give new graduate students maps to color, hoping to find one which seemed to require 5 colors. Of course each one got colored with 4 colors, but his faith did not waver. I have not seen this fervor in regard to the planes of order 10. I have seen papers which included theorems of the form "If there is a projective plane of order 10 then ....", but frequently they also included "If there does NOT exist ..." theorems as well. The point I am trying to make is more or less this: It is all well and good to give "objective" arguments about why computer proofs are valid or are not, but somehow those arguments wind up supporting what the speaker wanted to believe anyway! Bob Wilson ------------------------------ Date: Wed, 17 May 89 10:21:21 pdt From: Robert English Subject: Re: Computers in mathematical proofs I don't really see that much difference between a computerized proof and standard proof. In both cases, all steps of the proof must be rigorous. In a computerized proof, the mathematician must rigorously prove that his program is correct. In effect, the program definition becomes a lemma within the larger proof. Philosophical problems don't crop up until you ask whether the computer operated correctly, or whether defects in the underlying software (such as the compiler or the operating system) corrupted the results. Since the entire system does not admit rigorous examination, some claim that the process is fundamentally different than rigorous proof. What this argument overlooks is that rigor does not guarantee correct- ness to any greater degree than can be achieved in a computer-aided proof. A complicated proof can have errors at many stages, and reviewers cannot be trusted to find them all, any more than programmers can be trusted to find all of the bugs in a complicated computer system. Furthermore, while program proofs do not admit direct human verification, they do allow independent verification by other humans using similar, but different, tools. The question of whether independent verification actually takes place for program proofs is equivalent to the question of whether each step in a rigorous proof is really verified by independent auditors. In both cases, theoretical verification is possible, but in practice, it may not take place, or the auditing process may fail. --bob-- ------------------------------ Date: Mon, 15 May 89 15:35:22 EDT From: travis@douglass.cs.columbia.edu (Travis Lee Winfrey) Subject: Re: Computers in mathematical proofs >Lam himself says he was hoping for a positive result, which would be easy >to check, rather than a negative one. But he is fairly confident in his >result, citing two reasons: (a) the programs did do some internal >consistency checks; (b) the result agrees with "mathematical intuition" >(for example, an order-10 projective plane is known to be forbidden to >have any symmetry, which apparently is almost unheard-of for such an object). Is anyone more familiar with this work, such as any testing or proving techniques he attempted on his program? 100 trillion bug-free executions seems rather high, particularly given the binary nature of the answer he needed. Has the Lam proof been published yet? ------------------------------ Date: Thu, 11 May 89 16:43:21 -0400 From: leveson@LCS.MIT.EDU Subject: Formal Methods -- Call For Papers Given the forthcoming MoD standard in Great Britain requiring the use of formal methods on safety-critical software, we thought the following might be of interest to Risks readers. Call for Papers for Special Issues of IEEE Software, Computer, Transactions on Software Engineering: Formal Methods for Software Engineering Formal Methods are design and construction methods explicitly based on well-defined mathematical formalisms. Examples are: VDM, Z, box-structures, traces, predicate transformers, state transition systems, axiomatic data types, and many more. These methods promise (1) better control over the system development process through clarity and precision of specification and then of development steps and (2) reduced error commission and persistence through rigor, systematic review, and formal analysis. Much progress has been made in using formal methods, developing support systems for them, and evaluating their applicability on industrially-oriented problems. Applications to critical systems are appearing world-wide, and there is now some commercial interest based on advances in verifiable execution environments. Several standards groups are using formal methods and one - VDM - is undergoing the international standards process. A coordinated set of papers is planned for September 1990 with a survey plus a tutorial in IEEE Computer, application case studies in IEEE Software, and research papers in IEEE Transactions on Software Engineering. Oct. 1, 1989 Drafts Due (earlier submissions welcome) Mar. 1, 1990 Reviews Completed May 1, 1990 Revisions Completed September, 1990 Publication A complete call for papers containing detailed information about submission and content will be published in SEN (July) and each of the journals. Information and a copy of the complete call for papers is available from the editors: Applications, tutorial, survey: Research Contributions: Susan Gerhart Nancy Leveson MCC Software Technology Program Info. & Computer Science Dept. 3500 W. Balcones Dr. University of California Austin TX 78759, U.S.A. Irvine, CA 92717 Phone: 512-338-3492 Phone: 714-856-5517 Fax: 512-338-3899 Fax: 714-856-4056 e-mail: gerhart@mcc.com e-mail: nancy@ics.uci.edu ------------------------------ End of RISKS-FORUM Digest 8.73 ************************ -------