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.

Document type: Part of book or chapter of book

Full document

The PDF file did not load properly or your web browser does not support viewing PDF files. Download directly to your device: Download PDF document

Original document

The different versions of the original document can be found in:


DOIS: 10.1007/978-3-642-05089-3_35 10.1184/r1/6605798.v1 10.1184/r1/6605798

Back to Top

Document information

Published on 01/01/2018

Volume 2018, 2018
DOI: 10.1007/978-3-642-05089-3_35
Licence: CC BY-NC-SA license

Document Score

0

Views 3
Recommendations 0

Share this document

claim authorship

Are you one of the authors of this document?