Formal verification of lateral and temporal safety buffers for state-based conflict detection

This article presents an analytical definition of lateral and temporal safety buffers to be used in state-based conflict detection algorithms. A lateral buffer is a distance to be added to the minimum lateral separation to accommodate for uncertainty in the surveillance information. A temporal buffe...

Full description

Saved in:
Bibliographic Details
Published in:Proceedings of the Institution of Mechanical Engineers. Part G, Journal of aerospace engineering Journal of aerospace engineering, 2013-09, Vol.227 (9), p.1412-1424
Main Authors: Narkawicz, Anthony, Muñoz, César, Herencia-Zapana, Heber, Hagen, George
Format: Article
Language:English
Subjects:
Air traffic control
Algorithms
Buffers
Conflict resolution
Information
Mathematical models
Safety
Surveillance
Temporal logic
Theorem proving
Theorems
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:This article presents an analytical definition of lateral and temporal safety buffers to be used in state-based conflict detection algorithms. A lateral buffer is a distance to be added to the minimum lateral separation to accommodate for uncertainty in the surveillance information. A temporal buffer is a time to be added to the lookahead conflict detection time to accommodate for dropped surveillance messages due to signal attenuation. These safety buffers are defined using precise mathematical statements and the main theorems give numerical upper bounds on the probability of a missed alert. A particular case is considered where absolute bounds on the errors in position and velocity information are known. In this case, under well-defined assumptions provided in this article, safety buffers are given that guarantee mathematically that the probability of a missed alert is zero. The results are presented as theorems, which were formally proven using a mechanical theorem prover.
ISSN:0954-4100
2041-3025
DOI:10.1177/0954410012456495