Advertisement

Formal Verification of Conflict Detection Algorithms

  • Ricky Butler
  • Víctor Carreño
  • Gilles Dowek
  • César Muñoz
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2144)

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.

Keywords

Detection Algorithm Theorem Prove Bank Angle High Level Property Ground Speed 
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

  1. 1.
    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.Google Scholar
  2. 2.
    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.CrossRefGoogle Scholar
  3. 3.
    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.Google Scholar
  4. 4.
    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.Google Scholar
  5. 5.
    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.Google Scholar
  6. 6.
    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.Google Scholar
  7. 7.
    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.Google Scholar
  8. 8.
    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.Google Scholar
  9. 9.
    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.Google Scholar
  10. 10.
    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.Google Scholar
  11. 11.
    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.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Ricky Butler
    • 1
  • Víctor Carreño
    • 1
  • Gilles Dowek
    • 2
  • César Muñoz
    • 3
  1. 1.Assessment Technology BranchNASA Langley Research Center HamptonUSA
  2. 2.INRIA, Domaine de Voluceau - RocquencourtLe Chesnay CedexFrance
  3. 3.ICASENASA Langley Research Center HamptonUSA

Personalised recommendations