Path: utzoo!attcan!uunet!lll-winken!cs!shimeall
From: shimeall@cs.nps.navy.mil (Tim Shimeall)
Newsgroups: comp.software-eng
Subject: Re: "Program Proving"
Summary: Example reference
Message-ID: <950@cs.nps.navy.mil>
Date: 19 Mar 90 22:25:29 GMT
References: <12326@goofy.megatest.UUCP> <18261@duke.cs.duke.edu> <19989@joshua.athertn.Atherton.COM>
Reply-To: shimeall@cs.nps.navy.mil (Tim Shimeall)
Organization: Naval Postgraduate School, Monterey CA
Lines: 33

(sorry for the post -- I tried to reply directly but my mailer bounced
 your address)
In article <19989@joshua.athertn.Atherton.COM> you write:
>Can you please post 3-6 references to the controlled studies which show
>that formal proofs are a better way to budget time than debugging?

I can't post 3-6 references to such studies (in general, programming
experiments are so expensive to run that expecting several studies to
examine a single issue is VERY unrealistic) but I can point you to
one:

J.E. Brunelle and D.E. Eckhardt ``Fault Tolerant Software: Experiment
with the SIFT Operating System,'' {\it AIAA Computers in Aerospace V
Conference}, October 1985, pp. 355--360.

This study compared a portion of the verified SIFT kernel against two
independently developed versions (using a controlled development
procedure) of the kernel (all three developed from the same
specification).  They ran a large number of randomly-generated data
sets through the three versions.  The study found several faults in the
comercially-developed version, but NO faults in the verified version.

If you want to see 3-6 studies on this subject, may I suggest that you
(or your organization) sponsor such work.  But it isn't inexpensive
(you don't get something for nothing), especially if you wish to see
controlled studies done using industrial problems.  Such studies range
in cost from the hundreds of thousands of dollars to the millions of
dollars.  For comparison, I ran a testing study for my dissertation 
that involved 50+ people and took about 2 years of real time and slightly 
over a Sun/3 CPU-decade.  That was analyzing a set of 2000-line programs.  
NO ONE in the current environment is seriously planning to try controlled
development studies on large industrial problems -- the funds simply
aren't there.