EADIFD is written in symbolic assembly language for execution on the C4000 airborne computer. It is a subprogram of an aircraft navigation and guidance program and is used to generate pitch and roll command signals for use in terminal airspace. The proof of EADIFD was carried out by an inductive assertion method consisting of two parts, a verification condition generator and a source language independent proof checker. With the specifications provided by NASA, EADIFD was proved correct. The termination of the program is guaranteed and the program contains no instructions that can modify it under any conditions.


    Zugriff

    Zugriff über TIB

    Verfügbarkeit in meiner Bibliothek prüfen


    Exportieren, teilen und zitieren



    Titel :

    Proving the correctness of the flight director program EADIFD, volume 1


    Beteiligte:
    Lee, F. J. (Autor:in) / Maurer, W. D. (Autor:in)

    Erscheinungsdatum :

    01.07.1977


    Medientyp :

    Report


    Format :

    Keine Angabe


    Sprache :

    Englisch





    Proving Correctness of Autocoded Control Software

    Alegre, Fernando / Valenzuela, Rene / Feron, Eric et al. | AIAA | 2007


    Automatically proving the correctness of vehicle coordination

    Mikael Asplund | DOAJ | 2018

    Freier Zugriff

    Proving Correctness of Autocoded Control Software AIAA Paper

    Alegre, F. / Valenzuela, R. / Feron, E. et al. | British Library Conference Proceedings | 2007


    Proving the Correctness of Multicopter Rotor Fault Detection and Identification Software

    Bhaumik, Ankita / Dutta, Airin / Kopsaftopoulos, Fotis et al. | IEEE | 2021