An Approach to Formal Verification of Free-Flight Separation

This paper presents an approach to verifying complex free-flight algorithms. We give an abstract model that defines properties that a concrete implementation of a (distributed) free-flight algorithm has to maintain to guarantee conflict free movement of airplanes. We develop this model gradually by defining the emergent behavior of airplanes at a very abstract level and refine our definitions towards a more concrete model. In this process, we prove every refinement step to guarantee correctness of our approach.