Formal verification of curved flight collision avoidance maneuvers: A case study

@INPROCEEDINGS{DBLP:conf/fm/PlatzerC09,
	pdf = {pub/RCAS.pdf},
	slides = {pub/RCAS-slides.pdf},
	study = {pub/RCAS-examples.zip},
	TR = {DBLP:conf/fm/PlatzerC09:TR},

  author    = {Andr{\'e} Platzer and
               Edmund M. Clarke},
  title     = {Formal Verification of Curved Flight
               Collision Avoidance Maneuvers:
               A Case Study},
  booktitle = {FM},
  year      = {2009},
  pages     = {547-562},
  doi       = {10.1007/978-3-642-05089-3_35},
  editor    = {Ana Cavalcanti and
               Dennis Dams},
  longbooktitle = {FM 2009: Formal Methods, 16th
               International Symposium on Formal Methods,
               Eindhoven, Netherlands, November 2-6, 2009,
               Proceedings},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {5850},
  keywords  = {formal verification of hybrid systems,
               deduction, air traffic control,
               logic for hybrid systems},
  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.}
}```