Please try the URL privacy information feature enabled by clicking the flashlight icon above. This will reveal two icons after each link the body of the digest. The shield takes you to a breakdown of Terms of Service for the site - however only a small number of sites are covered at the moment. The flashlight take you to an analysis of the various trackers etc. that the linked site delivers. Please let the website maintainer know if you find this useful or not. As a RISKS reader, you will probably not be surprised by what is revealed…
(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.
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.
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.
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
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--
>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?
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
Please report problems with the web pages to the maintainer