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.
Formal verification of lateral and temporal safety buffers for state-based conflict detection
2013-09-01
13 pages
Article (Journal)
Electronic Resource
English
Formal verification of lateral and temporal safety buffers for state-based conflict detection
Online Contents | 2013
|FORMAL VERIFICATION OF SAFETY BUFFERS FOR STATE-BASED CONFLICT DETECTION AND RESOLUTION
British Library Conference Proceedings | 2010
|