Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study

Abstract

Aircraft collision avoidance maneuvers are important and complex applications. Curved flight exhibits nontrivial continuous behavior. In combination with the control choices during air traffic maneuvers, this yields hybrid systems with challenging interactions of discrete and continuous dynamics. As a case study illustrating the use of a new proof assistant for a logic for nonlinear hybrid systems, we analyze collision freedom of roundabout maneuvers in air traffic control, where appropriate curved flight, good timing, and compatible maneuvering are crucial for guaranteeing safe spatial separation of aircraft throughout their flight. We show that formal verification of hybrid systems can scale to curved flight maneuvers required in aircraft control applications. We introduce a fully flyable variant of the roundabout collision avoidance maneuver and verify safety properties by compositional verification.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Aug 01, 2009
Accession Number
ADA507059

Entities

People

  • AndrĂ© Platzer
  • Edmund M. Clarke

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • Air Platforms

DTIC Thesaurus Topics

  • Air Traffic
  • Aircrafts
  • Algorithms
  • Case Studies
  • Collision Avoidance
  • Collisions
  • Computational Complexity
  • Computer Science
  • Coordinate Systems
  • Differential Equations
  • Equations
  • Flight Paths
  • Free Flight
  • Hybrid Systems
  • Maneuvers
  • Partial Differential Equations
  • Verification

Readers

  • Aviation Safety and Air Traffic Management
  • Aviation Science / Aeronautics.
  • Mathematical Modeling and Probability Theory.