Industrial Applications of Formal Methods to Model, Design, and Analyze Computer Systems: An International Survey
Noyes Data Corporation, Nov 1, 1994 - Computers - 306 pages
Formal methods are mathematically-based techniques, often supported by reasoning tools, that can offer a rigorous and effective way to model, design and analyze computer systems. The purpose of this study is to evaluate international industrial experience in using formal methods. The cases selected are representative of industrial-grade projects and span a variety of application domains. The study had three main objectives:
· To better inform deliberations within industry and government on standards and regulations;
· To provide an authoritative record on the practical experience of formal methods to date; and
À To suggest areas where future research and technology development are needed.
This study was undertaken by three experts in formal methods and software engineering: Dan Craigen of ORA Canada, Susan Gerhart of Applied Formal Methods, and Ted Ralston of Ralston Research Associates. Robin Bloomfield of Adelard was involved with the Darlington Nuclear Generating Station Shutdown System case.
Support for this study was provided by organizations in Canada and the United States. The Atomic Energy Control Board of Canada (AECB) provided support for Dan Craigen and for the technical editing provided by Karen Summerskill. The U.S. Naval Research Laboratories (NRL), Washington, DC, provided support for all three authors. The U.S. National Institute of Standards and Technology (NIST) provided support for Ted Ralston.
What people are saying - Write a review
We haven't found any reviews in the usual places.
Other editions - View all
abstract achieve AECB AECL analysis approach automated CAS Logic checker CICS Cleanroom client COBOL/SF commercial communication components Context Control System cost Craigen DNGS documentation effort errors evaluation experience floating point Floating Point Unit formal methods formal specification GEC Alsthom hardware Hewlett-Packard Hoare Hoare Logic HP-SL Hursley impact implementation improved industrial INMOS interface Interview involved Labs Leveson lines of code Lloyd's Register machines mathematical methodology NIST notation object-oriented Occam OH and AECL Ontario Hydro operations organizations oscilloscope Pamas performed Praxis problems Processor program function tables prototype pseudo-code R&D Summary RAISE RATP refinement requirements reusable SACEM safety safety-critical schema SDS1 semantics shutdown system simulation smartcard software development Software Engineering specification language SSADM standard structure TBACS TCAS techniques Tektronix testing toolset Transputer Verification and Validation