Delivery-Date: 
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Message-Id: <9305111306.AA02891@air52.larc.nasa.gov>
Date: Tue, 11 May 93 09:06:21 -0400
From: Victor "A." Carreno <vac@air16.larc.nasa.gov>
To: joyce@cs.ubc.ca
Subject: Re: UK interim defence procurement standard 00-55
In-Reply-To: Mail from 'Jeffrey Joyce <joyce@cs.ubc.ca>' dated: 10 May 93 22:58 -0700
Cc: info-hol@ted.cs.uidaho.edu, vac@air16.larc.nasa.gov


Hi jeff,

> Also, does anyone know of other similar (proposed) industry
> or government standards requiring the use of formal methods ?

There is a publication which is widely used in the aeronautical community
for software certification. It is RTCA/DO-178B developed by RTCA subcommity
SC-167 and the European Organisation for Civil Aviation Equipment (EUROCAE)
WG-12. The use of formal methods is not required but can be used as an
alternative method for some verification procedures.

FAA Advisory Circular 20-115B states:
[...]
An applicant for a TSO authorization, TC, or STC for any electronic
equipment or system employing digital computer technology may use the
considerations outlined in RTCA Document RTCA/DO-178B as a means, but not
the only means, to secure FAA approval of the digital computer software.
[...]
[TSO = technical standard order]
[TC = type certification]
[STC = supplemental type certification]

In RTCA/DO-178B(1 DEC 1992):

Section 12. Additional Considerations
Subsection 12.3 Alternative Methods

Some methods were not discussed in the previous sections of this document
because of inadequate maturity at the time this document was written or
limited applicability for airborne software. It is not the intention of
this document to restrict the implementation of any current or future
methods. Any single alternative method discussed in this sectionnn is not
considered an alternative to the set of methods recommended by this
document, but may be used in satisfying one or more of the objectives in
this document. [...]

Sub-subsection 12.3.1 Formal Methods

Formal methods involve the use of formal logic, discrete mathematics, and
computer-readable languages to improve the specification and verification
of software. These methods could produce an implementation whose
operational behavior is known with confidence to be within a defined
domain. In their most thorough application, formal methods could be
equivalent to exhaustive analysis of a system with respect to its
requirements. [...]

Sub-subsection 12.3.1 is about one page long. If interested, I could send
you a copy.

Victor.