Research On The Key Technology Of C-to-MSVL Conversion System

C language is a general hither-level programming language.C language is widely used in system software and application software because of its flexibility,high efficiency,rich functions and strong portability.However,errors often occur in C programs,some of which may lead to serious consequences.With the increasing scale of software,it becomes more and more important to ensure the correctness and reliability of C programs.MSVL is a logic programming language based on Projection Temporal Logic,which can be used for large-scale software and hardware system verification.By transforming C program into MSVL program with the same semantics,and then modeling,simulating and verifying MSVL program,the correctness of the source C program can be indirectly verified.This thesis mainly studies the key issues in the implementation of C-to-MSVL transformation system.The main work is as follows:1.The similarities and differences between C language and MSVL language are studied.And the C language standard suitable for the transformation system,Xd-C,is defined.Then the main differences between Xd-C and ANSI C are explained,which provides a theoretical basis for subsequent works.2.The framework and execution flow of the system is optimized.And then the optimized system is introduced in detail.According to the function,the system is divided into five modules: preprocessing module,lexical analysis and parser module,transformation module,post-processing module and integration module.After that,the function and implementation details of each module are explicated specifically.3.The problems encountered in the implementation are solved.And the key problems such as function pointer problem,structure problem and custom type problem are described in detail.Then solutions are explained and implemented.4.The usage of the system is introduced by the transformation of Quick-Sort program.By comparing the consequences before and after transformation of anti_collision RFID and c JSON,the availability and practicability of C-to-MSVL transformation system are demonstrated.