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.


    Zugriff

    Zugriff über TIB

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    An approach to formal verification of free-flight separation


    Beteiligte:
    Eder, S. (Autor:in) / Smith, G. (Autor:in)


    Erscheinungsdatum :

    2010


    Format / Umfang :

    6 Seiten, 10 Quellen




    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Print


    Sprache :

    Englisch




    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