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 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.