FORMAL VERIFICATION OF SAFETY BUFFERS FOR STATE-BASED CONFLICT DETECTION AND RESOLUTION

摘要

There are always errors when measuring positionrnand velocity of moving objects such as aircraft.rnTherefore, the information provided by globalrnpositioning systems is never totally exact. Thisrnpaper studies the effects of these errors in the actualrnseparation of aircraft in the context of statebasedrnconflict detection and resolution. Assumingrnthat the state information is uncertain but thatrnbounds on the errors are known, this paper providesrnanalytical definitions of safety buffers andrnsufficient conditions under which these buffersrnguarantee that actual conflicts are detected andrnsolved. The results are presented as theorems,rnwhich were formally proven using a mechanicalrntheorem prover.