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.


    Access

    Access via TIB

    Check availability in my library


    Export, share and cite



    Title :

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


    Contributors:
    Lee, F. J. (author) / Maurer, W. D. (author)

    Publication date :

    1977-07-01


    Type of media :

    Report


    Type of material :

    No indication


    Language :

    English





    Proving Correctness of Autocoded Control Software

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



    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