|
|
|
home >
research >
contract work
Formal Methods: Past Program Sponsors
(Note: most of the following text comes directly from the June 2000 edition
of NASA Langley`s Research and Technology-Transfer Program
in Formal Methods, which is available in
PDF
(Download Adobe Acrobat Reader
if needed).
Aviation Safety Program
(AvSP)
- Rockwell Collins Advanced Technology Center:
The goal of the
Methods and Tools for
Flight Critical Systems project is to improve aviation safety by eliminating
defects early in the life-cycle, ensuring safety requirements are met,
reducing potential sources of operator confusion, and increasing the
sophistication of the systems we can safely deploy.
- Honeywell Engines and Systems: Combine new Time
Triggered Architecture (TTA) developed in Europe for the automotive
industry and formal verification methods to develop an FTIMA
architecture. Targeted application is Full Authority Digital Engine
Control (FADEC). Team includes SRI International and TTTech. See
- Barron Associates/Goodrich Aerospace: Develop verification methods
that can serve as a basis for certifying non-adaptive neural nets for
use on military and commercial aircraft.
See
- Hull, J.R., D.G. Ward,
"Verification and Validation of Neural Networks
for Safety-Critical Applications", Proc. American Control Conf.,
Anchorage, AK, May 8-10, 2002.
- Bateman, A.J., D.G Ward, and J.F. Monaco,
"Stability Analysis for Reconfigurable Systems with Actuator Saturation,"
Proc. American Control Conf., Anchorage, AK, May 8-10, 2002.
- University of Virginia/Northrup-Grumman
(formerly Litton):
Identify and develop methods and tools to
facilitate integration of formal verification methods into the
software development lifecycle within an aerospace company.
Computing, Information and Communications Technology Program
(CICT)
- Honeywell Technology Center (Minneapolis): Develop and implement
formal techniques for verifying the safety of IMA
software using the DEOS operating system as the test subject.
See EMSOFT02 Talk
and
Cofer, Darren; Engstrom, Eric; Weininger, N.; Penix, J.; Visser,
W.:
Using model checking for verification of partitioning properties in integrated modular avionics ,19th Digital Avionics Systems Conference, 7-13 October 2000,
Philadelphia, PA, p. 1D2/1-10.
John Rushby,
A Comparison of Bus Architectures for Safety-Critical Embedded Systems,
NASA/CR-2003-212161, March 2003, pp. 63.
SRI international (with a subcontract with Honeywell HTC):
Develop a customizable version of PVS Theorem Prover functionality.
SRI Matlab Project
Automatic Test Generation
Engineering for Complex Systems Program
(ECS)
- Accident Investigation CAUSE
- Hypatheon
Aerospace Vehicle System Technology Program
(AVSTO)
Advanced Air Transportation Technology Program
(AATT)
Advanced air traffic management concepts are being developed which
distribute the responsibility for traffic separation among
many different entities.
As a consequence, these concepts move some of the safety risk from
human controllers into on-board software and hardware systems. One
example of the new kind of distributed systems is air traffic conflict
detection and resolution. Traditional methods for safety assessment
such as human-in-the-loop simulations, testing, and flight experiments
may not be sufficient in this highly distributed system: the set of
possible scenarios is too large to have a reasonable coverage.
Our research seeks to apply formal methods to the safety assessment of
these critical avionics systems.
Small Aircraft Transportation System (SATS)
See FM Contractors
for more information about the contractors and links
to external web sites.
Note: The
tag identifies links that are outside of the NASA domain.
|
