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.
Formal Verification of Air Traffic Conflict Prevention Bands Algorithms
2010-06-01
Report
No indication
English
FORMAL VERIFICATION OF SAFETY BUFFERS FOR STATE-BASED CONFLICT DETECTION AND RESOLUTION
British Library Conference Proceedings | 2010
|Information Technology - Safety Analysis of Conflict Prevention Algorithms
Online Contents | 2014