Integrating informal and formal techniques to reverse engineer imperative programs.

摘要

Many well-documented computer failures have been attributed to software. Some of the most notable incidents include the catastrophic failures of the Therac-25 and the Ariane 5 spacecraft. A commonly overlooked aspect of these failures has been the fact that both were the result of an improper reengineering of software from one version to another.; The failure to correctly analyze software in both the Therac-25 and Ariane 5 resulted in catastrophic events that led to loss of life and property. These examples vividly illustrate the need for sophisticated and systematic methods for maintaining software in order to understand their functionality.; Reverse engineering of program code is the process of examining components and component interrelationships in order to construct a high-level abstraction of an implementation. Reengineering is the process of examination, understanding, and alteration of a system with the intent of implementing the system in a new form. Software reengineering is considered to be a better solution for handling legacy code as opposed to developing software from the original requirements. Since much of the functionality of the existing software has been achieved over a period of time, it must be preserved for many reasons, including providing continuity to current users of the software.; This research focuses on three primary contributions to the areas of software engineering and software maintenance. First, we have developed a technique for the construction of as-built formal specifications from program code using the strongest postcondition predicate transformer. Second, we have developed a formal technique for introducing abstraction into as-built specifications with the intent of obtaining design level specifications. Third, we have used the formal technique to support program understanding and software reuse activities.