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

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.

@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é Platzer', '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', '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.}
}