jbn@wdl1.UUCP (09/26/85)
The current state of the art in the verification field is worse than one may think from reading the literature. I have just obtained a copy of ``Peer Review of a Formal Verification/Design Proof Methodology'', (NASA Conference Publication 2377, NASA Langley Research Center, Scientific and Technical Information Branch, 1985), which is highly critical of SRI International's work in the area. The work being evaluated is SRI's verification of the Software Implemented Fault Tolerance system, a multiprocessor system intended for use in future aircraft flight control systems. Some quotes from the report: [p. 22] ``Scientific workers are expected to describe their accomplishments in a way that will not mislead or misinform. Members of the peer review panel felt that many publications and conference presentations of the SRI International verification work have not accurately presented the accomplishments of the project; several panel members, as a result of the peer review, felt that much of what they though had been done had indeed not been done.'' ``The research claims that the panel considered to be unjustified are primarily in two categories; the first concerns the methodology purportedly used by SRI International to validate SIFT, and the second concerns the degree to which the validation had actually been done. Many publications and conference presentations concerning SIFT appear to have misrepresented the accomplishments of the project.'' [p. 23] ``The incompleteness of the SIFT verification exercise caused concern at the peer review. Many panel members who expected (from the literature) a more extensive proof were disillusioned. It was the consensus of the panel that SRI's acomplishment claims were strongly misleading.'' John Nagle
jbn@wdl1.UUCP (09/26/85)
An attempt to post the previous message to the ARPANET AI mailing list (maintained by SRI International) resulted in the following reply: John Nagle Return-Path: <LAWS@SRI-AI.ARPA> Mail-From: SRI-AI.ARPA received by FORD-WDL1 at 26-Sep-85 10:07:52-PDT Date: Thu 26 Sep 85 10:05:12-PDT From: Ken Laws <Laws@SRI-AI.ARPA> Subject: Re: Peer review of SRI verification work To: jbn@FORD-WDL1.ARPA cc: AIList-Request@SRI-AI.ARPA Reply-To: AIList-Request@SRI-AI.ARPA In-Reply-To: Message from "jbn@FORD-WDL1.ARPA" of Tue 24 Sep 85 17:55:59-PDT The quotations in your message seem to indicate a lack of professionalism or competence, or at least of communication skills, on the part of some group at SRI. It seems a little strained to indict the entire field of software verification on the basis of that one project, but you are entitled to make the point. I haven't figured out yet what this has to do with AI. Are you picking up on the mention of SDI in AIList and trying to say that SDI verification is an Achilles' heel? If so, ARMS-D@MIT-MC would seem to be the appropriate list. If you are commenting on software engineering in general, SOFT-ENG@MIT-XX would be more appropriate. If you are making a point about the way "science" is done in this country, Phil-Sci%MIT-OZ@MIT-MC would be the proper list. If you wish your message to appear in AIList, I will have to ask that you modify the message to clarify your point and its relevance to the AIList readership. -- Ken Laws -------
johnson@uiucdcsp.CS.UIUC.EDU (09/30/85)
Where I come from (Cornell) verification is thought to have no more relationship to AI than compiler-compilers have to AI. I am glad to see that some AI people also have that opinion. That said, I found the excerpt from the peer review very interesting. I will certainly try to find the original reference. Could the original poster please send the message to SOFT-ENG@MIT-XX? Ralph Johnson