Design And Implementation Of C-to-MSVL Program Transformation System

Currently, C language is one of the most mainstream programming languages, and has been widely used in various fields of software design. However, a series of errors often appear in C programs, such as array bound and dividing zero problems, which will cause program errors and even system collapse. Therefore, it is important to ensure the correctness of C programs. As a rigious approach, formal verification verifies the correctness of systems through checking whether a system satisfies its specifications with the associated mathematical theory. It can ensure the correctness of systems in a fundamental way. The temporal logic language MSVL is a Modeling, Simulation and Verification Language used in formal verification, it has been suceessfully applied to the specification and verification of real-time systems.This thesis is mainly concerned with the design and implementation of C-to-MSVL program transformation system; the author?s major contributions are outlined as follows:1. The principle of C program model checking tools is studied. Some deficiencies of those tools are pointed out, such as it is difficult to guarantee the consistency between the extracted model and program. This thesis presents a method to verify the correctness of C programs with MSVL. Firstly, C program is translated to MSVL program which is treated as the model of C program. In this way, to verify the correctness of C programs is changed to verify the correnctness of MSVL programs. Secondly the properties of system are described with Propositional Projection Temporal Logic(PPTL). Finally the targed MSVL programs are simulated and verified with the MSV interpreter.2. The knowledge of C language and MSVL is studied. In this thesis, transformation rules from C programs to MSVL programs are designed and given by means of analyzing the similarities and differences between C language and MSVL.3. Based on the existing compilers and transformation systems, the basic framework is designed and five modules are obtained in this system. The design plans of those modules are proposed and the C-to-MSVL program transformation system is developed in Visual C++ & Lex & Yacc.4. Two C programs are provided as examples to show the feasibility and practicability of our technique. One of them is "wolf-sheep-vegetables" problem, it shows the transformation process of C-to-MSVL program transformation system. It also illustrates the feasibility of our system through simulating and verifying the MSVL program with the MSV interpreter. The other program is "combinatorial number 24" problem, array bound and dividing zero problems are found in this problem through simulating the targed MSVL program. This case illustrates the practicability of C-to-MSVL transformation system.