(AILS) is a research project within the Reduced
Spacing Operations (RSO) element of the Terminal Area Productivity
(TAP) Program at NASA. The objective of the AILS research is to
increase the ability of aircraft to land on closely-spaced parallel
runways in Instrument Meteorological Conditions (IMC). The current
minimum runway separation for independent landings during IMC is
4300 feet. Using AILS, independent parallel approaces down to 2500
feet separation are expected to be possible. The AILS system is an
airborne alerting system that uses Automatic Dependent
Surveillance-Broadcast (ADS-B) datalink and differential GPS.
The AILS concept consists of accurate traffic
information visible at the navigation display and an alerting
algorithm which warns the crew when one of the aircraft involved in
a parallel landing is diverting from the intended flight path.
The inhouse project is exploring the use formal methods to
analytically demonstrate that the AILS alerting algorithm complies
with its requirements for all possible parallel landing scenarios.
The formalization
is conducted in the Prototype
Verification System (PVS)
. A PVS dump file of the AILS work is available here.
- César Muñoz, Víctor Carreño, Gilles Dowek, and Ricky Butler,
Formal Verification of Conflict Detection Algorithms,
Software Tools for Technology Transfer, Vol. 4, No. 3, 2003.
BibTeX
Reference.
Extended version available as NASA Technical Memorandum,
NASA/TM-2001-210864, May 2001.
BibTeX
Reference.
- Víctor Carreño and
César Muñoz, Aircraft Trajectory Modeling and Alerting
Algorithm Verification, Proceedings of the 13th International
Conference on Theorem Proving in Higher Order Logics (TPHOLs 2000),
Lecture Notes in Computer Science, Vol. 1869, 2000.
BibTeX
Reference.
Extended version available as NASA Contractor Report,
ICASE Report 2000-16, April 2000. BibTeX Reference.
- Víctor Carreño and
César Muñoz, Formal
Analysis of Parallel Landing Scenarios,
Proceedings of the 19th
Digital Avionics Systems Conference (DASC 2000), 2000. BibTeX
Reference.
Note: The tag identifies links that are outside
of the NASA domain.
