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.


    Access

    Access via TIB

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    An approach to formal verification of free-flight separation


    Contributors:
    Eder, S. (author) / Smith, G. (author)


    Publication date :

    2010


    Size :

    6 Seiten, 10 Quellen




    Type of media :

    Conference paper


    Type of material :

    Print


    Language :

    English




    Formal Verification of Flight Critical Software

    Miller, Steven / Anderson, Elise / Wagner, Lucas et al. | AIAA | 2005


    Towards Formal Verification of a Separation Microkernel

    Butterfield, A. / Sanan, D. / Hinchey, M. et al. | British Library Conference Proceedings | 2013


    Formal Verification of Quadcopter Flight Envelop Using Theorem Prover

    Jasim, Omar A. / Veres, Sandor M. | IEEE | 2018