Using Formal Methods and Object-Oriented Analysis to Reverse Engineer Shuttle SoftwareThis 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.