Formal Verification of AILS
The Airborne Information for Lateral Spacing (AILS) program at NASA Langley Research Center aims at giving pilots the information
necessary to make independent approaches to parallel runways with spacing down to 2500 feet in Instrument Meteorological Conditions.
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. We have developed a model of aircraft
approaches to parallel runways. Based on this model, we analyze the alerting algorithm with the objective of verifying its correctness. The
formalization is conducted in the general verification system PVS.
- Formal verification of conflict detection
algorithms, César Muñoz, Ricky Butler, Víctor Carreño,
and Gilles Dowek, Software Tools for Technology Transfer, BibTeX
Reference, 2003. Extended
version available as NASA/TM-2001-210864, BibTeX
Reference, 2001.
- Aircraft Trajectory Modeling and Alerting Algorithm Verification, Víctor Carreño and César Muñoz,
Proceedings
of the 13th International Conference on Theorem Proving in Higher Order
Logics, TPHOLs 2000, BibTeX
Reference, 2000. Extended version available as
ICASE Report 2000-16, BibTeX
Reference, 2000.
- Formal Analysis of Parallel Landing Scenarios, Víctor Carreño and César Muñoz,
Proceedings
of the 19th Digital Avionics Systems Conference, DASC 2000, BibTeX
Reference 2000.
Maintained by:
César A. Muñoz