On the Formal Verification of the TCAS Conflict Resolution Algorithms

Details

• Creators:
  Lygeros, John ; Lynch, Nancy
• Corporate Creators:
  Massachusetts Institute of Technology. Laboratory for Computer Science
• Subject/TRT Terms:
  • Traffic alert and collision avoidance system
  • Validation
  • Aviation safety
  • Air traffic control
  • Safety
  • Mathematical models
  • Conflict detection
  • Hybrid systems
  • Resolution advisories
• Resource Type:
  Research Paper
• Geographical Coverage:
  United States
• TRIS Online Accession Number:
  00748699
• Corporate Publisher:
  University of California, Berkeley. Robotics and Intelligent Machines Laboratory. Air Traffic Management Systems Program
• Abstract:
  PostScript file. TCAS is an on-board protocol for detecting conflicts between aircraft and providing resolution advisories to the pilots. Because of its safety-critical role the TCAS software should ideally be "verified" before it can be deployed. The verifcation task is challenging, due to the complexity of the TCAS code and the hybrid nature of the system. We show how the essence of this very complicated problem can be captured by a relatively simple hybrid model, amenable to formal analysis. We then outline a methodology for establishing conditions under which the advisories issued by TCAS are safe.
• Format:
  PDF
• Download URL:
  https://rosap.ntl.bts.gov/view/dot/38144/dot_38144_DS1.pdf
• File Type:
  [PDF - 154.64 KB]
• Collection(s):
  US Transportation Collection
• Main Document Checksum:
  urn:sha256:9263f003f204c9e2364ebdb95df4bb133f737f1e23e7e142438ecb40f143914a