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.
Applying Formal Methods and Object-Oriented Analysis to Existing Space Shuttle Software
1994-01-01
Preprint
No indication
English
Formal modeling of space shuttle software change requests using SCR
Tema Archive | 1999
|Generation of Object-Oriented Formal Software Specifications
British Library Conference Proceedings | 1997
|