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.
An approach to formal verification of free-flight separation
2010
6 Seiten, 10 Quellen
Conference paper
English
Formal Verification of Flight Critical Software
AIAA | 2005
|Towards Formal Verification of a Separation Microkernel
British Library Conference Proceedings | 2013
|Stability flight test verification by modal separation
AIAA | 1988
|