Dependence Analysis In Program Verification And Legacy System Reengineering By

Among the most measures ensuring reliability and security of softwares, computer scientists generally employ formalization methods to verify software systems. Currently, Computer-based verification can be divided into two kinds: the logic reasoning based theorem-proof, and the exhaustive search based model-checking. Compared to the latter approach, the automation degree of the former one is inferioer. However, because of its powerful expressiveness ability and gradually development of its automated theorem-proof technology, the former approach still owns better prospect. With this, it becomes the main approach attracting most researchers. On the other hand, most of the program verification process executed orderly with each verification rules. However, because of the concurrent characteristics of the verification process has not been fully tapped, the method severely restricts the efficiency of the verification work, particularly in the case of large programs. Therefore, to improve the efficiency of the verification process from the perspective of the concurrent degree program verification is meaningful.With the fast development of computer software industry, the generations of the most new technologies incur a lot of legacy systems. For this problem, there exist two ways to handle, designing a new system to replace a legacy system and reengineering it. These legacy systems are with: outdated technologies, unstructured architectures, lacking documents, high maintenance cost, etc... . Currently, many enterprises and organizations choose to utilize new software/hardware platform with modern technology to reengineer the legacy system to high reliability, high reusability, high maintainability and high performance of the system. Good system architecture design and scalability will become more and more important for every advanced system will eventually become a legacy system. Early systems generally resort procedure-oriented design, which is characterized by a functional implementation. The design focuses on business processes and ways to couple tightly with the system operations, is not benefit to system maintenance and upgrade. Therefore, it is meaningful to enhance the system scalability through converting process-oriented systems which focus on the realization to object-oriented systems which emphasize structure design.Because everything is related to each other, making use of the inter-dependence of things to carry out theoretical and applied research referred to not only universal realistic sense, but also potential academic value. To this end, this paper focuses on legacy systems reengineering and parallel programming verification strategy with the dependency analysis. The main contributions include:1. Proposes an algorithm to extract the control structure for While-program, and demonstrates its correctness and efficiency, and simply analizes the algorithm.2. Based on the dependency relationship between program's control structures, the paper proposes a parallel verification strategy to enhance the efficiency of the programs vierification, and further demonstrates the correctness and efficiency of the strategy.3. Applies the dependency analysis idea to the legacy systems reengineering process of converting process-oriented systems to object-oriented systems. In addition, the paper proposes a division method for the program modules based on dependency analysis and, improves a method to identify domain variables. Lastly, the amentioned method is employed to the transform process of the While-program to an instance in a Java-program.