Abstract
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 on the navigation display and an alerting algorithm which warns the crew when one of the aircraft involved in a parallel landing is diverting from its intended flight path. In this paper we present 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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
B. Dutertre. Elements of mathematical analysis in PVS. In J. Von Wright, J. Grundy, and J. Harrison, editors, Ninth international Conference on Theorem Proving in Higher Order Logics TPHOL, volume 1125 of Lecture Notes in Computer Science, pages 141–156, Turku, Finland, August 1996. Springer Verlag.
W. Chan, R. Anderson, P. Beame, and D. Notkin. Improving efficiency of symbolic model checking for state-based system requirements. Technical Report TR-98-01-03, University of Washington, Department of Computer Science and Engineering, January 1998.
T. Doyle and F. McGee. Air traffic and operational data on selected u.s. airports with parallel runways. Technical Report NASA/CR-1998-207675, NASA, May 1998.
B. Fuchssteiner. MuPAD User’s Manual. John Wiley and Sons, Chichester, New York, first edition, March 1996. Includes a CD for Apple Macintosh and UNIX.
M.P.E. Heimdahl and N.G. Leveson. Completeness and Consistency Analysis of State-Based Requirements. In Proceedings of the 17th International Conference on Software Engineering, pages 3–14, April 1995.
S. Koczo. Coordinated parallel runway approaches. Technical Report NASA-CR-201611, NASA, October 1996.
N.G. Leveson, M.P.E. Heimdahl, H. Hildreth, and J.D. Reese. Requirements specification for process-control systems. Technical Report ICS-TR-92-106, University of California, Irvine, Department of Information and Computer Science, November 1992.
A.M. Lind. Two simulation studies of precision runway monitoring of independent approaches to closely spaced parallel runways. Technical Report AD-A263433 ATC-190 DOT/FAA/NR-92/9, NASA, March 1993.
J. Lygeros and N. A. Lynch. On the formal verification of the TCAS conflict resolution algorithms. In Proceedings 36th IEEE Conference on Decision and Control, San Diego, CA, pages 1829–1834, December 1997. Extended abstract.
U. Martin and H. Gottliebsen. Computational logic support for differential equations and mathematical modeling. Personal communication, 2000.
S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In Deepak Kapur, editor, 11th International Conference on Automated Deduction (CADE), volume 607 of Lecture Notes in Artificial Intelligence, pages 748–752, Saratoga, NY, June 1992. Springer-Verlag.
L. Rine, T. Abbott, G. Lohr, D. Elliott, M. Waller, and R. Perry. The flight deck perspective of the NASA Langley AILS concept. Technical Report NASA/TM-2000-209841, NASA, January 2000.
RTCA. Minimum operational performance standards for traffic alert and collision avoidance system (TCAS) airborne equipment — consolidated edition. Guideline DO-185, Radio Technical Commission for Aeronautics, One McPherson Square, 1425 K Street N.W., Suite 500, Washington DC 20005, USA, 6 September 1990.
G. Wong. Development of precision runway monitor system for increasing capacity of parallel runway operations. AGARD, Machine Intelligence in Air Traffic Management, page 12, October 1993.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Carreño, V., Muñoz, C. (2000). Aircraft Trajectory Modeling and Alerting Algorithm Verification. In: Aagaard, M., Harrison, J. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2000. Lecture Notes in Computer Science, vol 1869. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44659-1_6
Download citation
DOI: https://doi.org/10.1007/3-540-44659-1_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67863-2
Online ISBN: 978-3-540-44659-0
eBook Packages: Springer Book Archive