FM Past Program: Navigation Specification
This page is not maintained.
It is probably out of date.
A cooperative research effort was initiated in 1993 with
Honeywell Air Transport Systems Division (Phoenix)
to study the incorporation of formal methods into the company's
software development processes.
In the initial project in this effort, NASA Langley funded ORA
to identify a component of the
Boeing 777
system to which formal
specification techniques could be applied, and to develop the formal
specifications for that component.
ORA, in collaboration with personnel from Langley and Honeywell, chose the
navigation subsystem as a suitable application.
Using documents supplied to them by Honeywell, ORA developed a specification
that addressed the following aspects of navigation:
- basic mathematical concepts such as functions over the reals,
and physical units such as distance, velocity, and acceleration
- definition of objects such as aircraft, radios, sensors, navigation aids,
and the navigation database
- definition of algorithms such as complementary filter processing,
navigation aid selection, navigation mode selection, and position
determination
- relating the mathematical model to Ada by partitioning the system in Ada
package specifications, and
annotating individual Ada functions and procedures with formal
specifications
The specification was done using ORA's
Penelope tool.
Curator and Responsible NASA Official: C. Michael Holloway
last modified: 2 August 2000 (10:13:28)
