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.


    Access

    Access via TIB

    Check availability in my library


    Export, share and cite



    Title :

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


    Contributors:
    A. Platzer (author) / E. M. Clarke (author)

    Publication date :

    2009


    Size :

    32 pages


    Type of media :

    Report


    Type of material :

    No indication


    Language :

    English




    Formal Verification of Collision Avoidance for Turning Maneuvers in UAVs

    Adler, Eytan / Jeannin, Jean-Baptiste | AIAA | 2019


    AIAA-2019-2845: Formal Verification of Collision Avoidance for Turning Maneuvers in UAVs

    Adler, Eytan / Jeannin, Jean-Baptiste | British Library Conference Proceedings | 2019




    Probability Based Optimal Collision Avoidance Maneuvers

    Kelly, Brad / De Picciotto, Solomon | AIAA | 2005