Number SRI-CSL-95-1.
Computer Science Laboratory, SRI International, Menlo Park, CA.
March, 1995.

This report is based on one prepared as a chapter for the FAA Digital Systems Validation Handbook (a guide to assist FAA Certification Specialists with Advanced Technology Issues). Its purpose is to explain the use of formal methods in the specification and verification of software and hardware requirements, designs, and implementations, to identify the benefits, weaknesses, and difficulties in applying these methods to digital systems used in critical applications, and to suggest factors for consideration when formal methods are offered in support of certification.

The presentation concentrates on the rationale for formal methods and on their contribution to assurance for critical applications within a context such as that provided by DO-178B (the guidelines for software used on board civil aircraft); it is intended as an introduction for those to whom these topics are new. A more technical discussion of formal methods is provided in a companion report (see link below).

@techreport{Rushby95:FAA,
    AUTHOR = {John Rushby},
    TITLE = {Formal Methods and their Role in the Certification of Critical Systems},
    INSTITUTION = {Computer Science Laboratory, {SRI} International},
    YEAR = {1995},
    NUMBER = {{SRI-CSL-95-1}},
    ADDRESS = {Menlo Park, {CA}},
    MONTH = {mar},
    NOTE = {Also available as {NASA} Contractor Report 4673, August 1995, and to be issued as part of the {FAA} Digital Systems Validation Handbook (the guide for aircraft certification).},
    URL = {http://www.csl.sri.com/papers/csl-95-1/}
}

• csl-95-1.dvi.gz
• csl-95-1.ps.gz
• tutorial-slides.ps.gz