This paper describes the application of formal methods and object-oriented modeling to reverse engineering, in which formal specifications are developed for existing, or legacy, code. In this project, several layers of formal specifications were constructed for a portion of the NASA Space Shuttle Digital Auto Pilot (DAP), a software module that is used to control the position of the spacecraft through appropriate jet firings.


    Access

    Access via TIB

    Check availability in my library


    Export, share and cite



    Title :

    Applying Formal Methods and Object-Oriented Analysis to Existing Space Shuttle Software


    Contributors:
    Cheng, B. (author) / Auernheimer, B. (author)

    Publication date :

    1994-01-01


    Type of media :

    Preprint


    Type of material :

    No indication


    Language :

    English





    Formal modeling of space shuttle software change requests using SCR

    Wiels, V. / Easterbrook, S. | Tema Archive | 1999


    Generation of Object-Oriented Formal Software Specifications

    Karagias, T. / Hartrum, T. / IEEE | British Library Conference Proceedings | 1997



    Space Shuttle software

    Sheridan, C.T. | Tema Archive | 1978