Using Formal Methods and Object-Oriented Analysis to Reverse Engineer Shuttle Software

Correctness is an important issue in safety-critical software control systems. Unfortunately, failures in critical segments of software for medical equipment, communications, and defense are familiar to the public. Such incidents motivate the use of software development techniques that reduce errors and detect defects. The benefits of applying formal methods in requirements-driven software development (forward engineering) are well-documented; formal notations are precise, verifiable, and facilitate automated processing. This paper describes the application of formal methods and objectoriented 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. The reverse engineering process was facilita..