Research On Application Of Formal Method To Reverse Engineering

With the rapid development of computer technology, more and more legacy systems were produced. Maintaining and upgrading these systems have long been a problem faced by software engineers. It is necessary to use the technology of reverse engineering to analysis the structure and behavior of the current system in order to maintain and re-engineering the legacy systems. Reverse engineering is the process of analyzing a system to identify the components and their relationships and create representations of the system in another form or at a higher level of abstraction, which can help engineers understand and reconstruct software system.Formal methods in software development provide many benefits in the forward engineering. A benefit of formal methods is that their notations are well-defined and thus, are amenable to automated processing.One method for introducing formal methods, and therefore taking advantage of the benefits of formal methods is through the reverse engineering of existing program code into formal specifications.This paper describes an approach to reverse engineering based on the formal semantics of the strongest postcondition predicate transformer,and the partial correctness model of program semantics introduced by Hoare. The main point of our investigation is how to use informal and formal methods for reverse engineering. The approach provided by this thesis is mainly to process the C program system for reverse engineering. In the thesis we defined the assignment rule, alternation rule, iteration rule, sequence rule and function rule according to the basic syntax structures of C programs and set up an axiom system of C programs. The process of reverse engineering is introduced through an instance, C-Minus (a simplified C language). In reverse engineering, the abstract syntax tree is generated by lexical analysis and syntax analysis from source code. The template information is extracted from structured source code, which is represented by a binary tree. Then the binary tree is translated into the P A D (Problem Analysis Diagram) according to the designed algorithm. After structured analysis, the statements of key source code will be scanned, and each statement will be translated into formal specification according to the strongest postcondition semantics of the basic structure.