From csus.edu!decwrl!decwrl!olivea!uunet!pipex!uknet!comlab.ox.ac.uk!ora.on.ca Wed Jul 28 07:19:19 1993 Newsgroups: comp.specification.z Path: csus.edu!decwrl!decwrl!olivea!uunet!pipex!uknet!comlab.ox.ac.uk!ora.on.ca From: dan@ora.on.ca (Dan Craigen) Subject: Report on an International Survey of Industrial Applications of FM Message-ID: <9307271859.AA23169@alpha.ora.on.ca> Sender: dan@ora.on.ca Date: Tue, 27 Jul 93 14:59:58 EDT X-Mailer: mail-news 2.0.3 Lines: 138 An International Survey of Industrial Applications of Formal Methods by Dan Craigen, Susan Gerhart and Ted Ralston NIST (National Institute of Standards and Technology) has published a survey of twelve case studies of the use of formal methods in industrial projects. The report is available in both paper and electronic forms; see details below. The project was sponsored by the U.S. NIST, the U.S. Naval Research Laboratory, and the Canadian Atomic Energy Control Board. The final report consists of two separate volumes. Volume 1 describes the purpose, approach, analysis, and conclusions of the survey; Volume 2 describes the case studies. The twelve cases that were surveyed are: o the use of the Software Cost Reduction methodology on the decision making logic for the shutdown systems of the Canadian Darlington Nuclear Generating Station. o the use of the Gypsy Verification Environment and Trust Domains to describe security properties of an Internet device for the transmission of datagrams. o the use of B to demonstrate safety properties of an automated train protection system. o the use of a variant of Statecharts, augmented with a tabular notation, to express the collision avoidance logic and surveillance subsystems of the U.S. TCAS (Traffic Alert and Collision Avoidance System). o the use of Z on IBM Hursley's CICS product. o the use of Cleanroom on a COBOL structuring program and a satellite attitude control system. o the use of Z to develop a software infrastructure for a family of oscilloscopes. o the use of Z and other formal techniques in the development of components for various generations of transputers. o the use of Z in developing a CASE tool for SSADM. o explorations of the use of RAISE through the ESPRIT funded LaCoS project. o the use of FDM (Formal Development Methodology) to specify security properties of a smartcard-based application. o the use of a VDM-derivative (HP-SL) on a real-time database. Electronic Version ------------------ The report is available in ASCII, PostScript, and WordPerfect formats. These files are accessible via Internet/Anonymous FTP, mail server, and Internet/XGopher. Volume 1 has 115 pages and Volume 2 has 188 pages, so you may want to transfer the files overnight. The report is contained in the pub/ahis/formal_methods directory at nemo.ncsl.nist.gov. The following files are contained in this directory: vol1.ps.Z Volume 1 in PostScript format vol1.wp Volume 1 in WordPerfect format vol1.txt Volume 1 in ASCII format vol2.ps.Z Volume 2 in PostScript format vol2.wp Volume 2 in WordPerfect format vol2.txt Volume 2 in ASCII format There is a README file that provides further details and options for retrieving the files. Paper Copies ------------ Order from National Technical Information Service 5285 Port Royal Road Springfield, Virginia 22161 U.S.A. Phone +1 703 487 4650 MUST Use the PB numbers to order: "An International Survey of InDustrial Applications of Formal Methods Volume 1 Purpose, Approach, Analysis and Conclusions" NIST GCR 93/626-V1 PB93-178556/AS Hard Copy: A07/$27.00 Microfiche: A02 $12.50 "An International Survey of Industrial Applications of Formal Methods Volume 2 Case Studies" NIST GCR 93-626-V2 PB93-178564/AS Hard Copy: A09/$27.00 Microfiche: A03/$12.50 Summaries --------- Papers have been published in the following: Formal Methods Europe, April 1993, "Formal Methods Reality Check: Industrial Applications" Proceedings by Springer Verlag 15th International Conference on Software Engineering, May 1993, "Observations on Industrial Practice Using Formal Methods" 7th Annual Z User Workshop "An International Survey of Industrial Applications of Formal Methods" A general briefing on the results of the study is available from the authors. Authors: --------- Dan Craigen, ORA Canada, Ottawa, Ontario, Canada dan@ora.on.ca +1 613 238 7900 Susan Gerhart, Applied Formal Methods, Inc., Austin, Texas, U.S.A. pl0183@mail.psi.net (now at RICIS, U. Houston at Clear Lake, Houston, Texas) +1 713 283 3800 Ted Ralston, Ralston Research Associates, Tacoma Washington, U.S.A. ralston@cli.com +1 206 759 3240