In air traffic management, a pairwise conflict is a predicted loss of separation between two aircraft, referred to as the ownship and the intruder. A conflict prevention bands system computes ranges of maneuvers for the ownship that characterize regions in the airspace that are either conflict-free or 'don't go' zones that the ownship has to avoid. Conflict prevention bands are surprisingly difficult to define and analyze. Errors in the calculation of prevention bands may result in incorrect separation assurance information being displayed to pilots or air traffic controllers. This paper presents provably correct 3-dimensional prevention bands algorithms for ranges of track angle; ground speed, and vertical speed maneuvers. The algorithms have been mechanically verified in the Prototype Verification System (PVS). The verification presented in this paper extends in a non-trivial way that of previously published 2-dimensional algorithms.


    Zugriff

    Zugriff über TIB

    Verfügbarkeit in meiner Bibliothek prüfen


    Exportieren, teilen und zitieren



    Titel :

    Formal Verification of Air Traffic Conflict Prevention Bands Algorithms


    Beteiligte:

    Erscheinungsdatum :

    2010-06-01


    Medientyp :

    Report


    Format :

    Keine Angabe


    Sprache :

    Englisch




    Formal Verification of a Conflict Resolution and Recovery Algorithm

    Maddalon, Jeffrey / Butler, Ricky / Geser, Alfons et al. | NTRS | 2004


    Formal Verification of a Conflict Resolution and Recovery Algorithm

    J. Maddalon / R. Butler / A. Geser et al. | NTIS | 2004


    Green conflict prevention device for traffic lights

    WANG CHUAN / WANG SHIYUAN | Europäisches Patentamt | 2022

    Freier Zugriff