Abstract
Safety assessment of new air traffic management systems is a main issue for civil aviation authorities. Standard techniques such as testing and simulation have serious limitations in new systems that are significantly more autonomous than the older ones. In this paper, we present an innovative approach for establishing the correctness of conflict detection systems. Fundamental to our approach is the concept of trajectory, which is described by a continuous path in the x-y plane constrained by physical laws and operational requirements. From the model of trajectories, we extract, and formally prove, high level properties that can serve as a framework to analyze conflict scenarios. We use the AILS (Airborne Information for Lateral Spacing) alerting algorithm as a case study of our approach.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
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.
V. Carreño and C. Muñoz. Aircraft trajectory modeling and alerting algorithm verification. In J. Harrison and M. Aagaard, editors, Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000, volume 1869 of Lecture Notes in Computer Science, pages 90–105. Springer-Verlag, 2000. An earlier version appears as report NASA/CR-2000-210097 ICASE No. 2000-16.
G. Dowek, C. Muñoz, and A. Geser. Tactical conflict detection and resolution in a 3-D airspace. Technical Report NASA/CR-2001-210853 ICASE Report No. 2001-7, ICASE-NASA Langley, ICASE Mail Stop 132C, NASA Langley Research Center, Hampton VA 23681-2199, USA, April 2001.
J. Kuchar and Jr. R. Hansman. A unified methodology for the evaluation of hazard alerting systems. Technical Report ASL-95-1, ASL MIT Aeronautical System Laboratory, January 1995.
J. Kuchar and L. Yang. Survey of conflict detection and resolution modeling methods. In AIAA Guidance, Navigation, and Control Conference, volume AIAA-97-3732, pages 1388–1397, New Orleans, LA, August 1997.
J. Lygeros and N. 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.
C. Muñoz, R.W. Butler, V. Carreño, and G. Dowek. On the verification of conflict detection algorithms. Technical Report NASA/TM-2001-210864, NASA Langley Research Center, NASA LaRC Hampton VA 23681-2199, USA, May 2001.
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.
Radio Technical Commission for Aeronautics. Final report of the RTCA board of directors’ select committee on free flight. Technical Report Issued 1-18-95, RTCA, Washington, DC, 1995.
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.
C. Tomlin, G. Pappas, and S. Sastry. Conflict resolution for air traffic management: A study in multi-agent hybrid systems. IEEE Transactions on Automatic Control, 43(4), April 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Butler, R., Carreño, V., Dowek, G., Muñoz, C. (2001). Formal Verification of Conflict Detection Algorithms. In: Margaria, T., Melham, T. (eds) Correct Hardware Design and Verification Methods. CHARME 2001. Lecture Notes in Computer Science, vol 2144. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44798-9_31
Download citation
DOI: https://doi.org/10.1007/3-540-44798-9_31
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42541-0
Online ISBN: 978-3-540-44798-6
eBook Packages: Springer Book Archive