Research And Implementation Of Modeling In MSVL Complier

With the popularization of computers in all areas of human society,the correctness of hardware and software systems has attracted lots of attentions.In the past decades,formal verification methods have become an important way to ensure the correctness of software and hardware systems.Because of its simplicity and unambiguous,temporal logic has been widely used in formal verification.As one kind of temporal logic programming language,MSVL is an executable subset of PTL,which can simulate,model and verify hardware and software systems.Among them,as the foundation of verification,the modeling method acts an extremely important role in MSVL.Tools designed for the implementation of programming languages are mainly divided into two kinds including compilers and interpreters.A compiler costs less time and memories than an interpreter.Therefore,this thesis focuses on how to build a model for an MSVL program in the compiler structure.In the modeling function for an MSVL program,the execution of the program can be shown simply and clearly,while the variables' changes can be described accurately,which is convenient for the subsequent verification work.The main contribution of this thesis is to propose the design framework of the modeling method,and put forward the solution to the key problems in the implementation of the framework.Based on the LLVM compiler system platform and MSVL semantics,MSVL statements are transformed into intermediate code(IR)with the dynamic control mechanism.Subsequently,executable files are generated through the linker.Finally,the program's model can be obtained.During the implementation of the framework,four key technologies are put forward based on characteristics of MSVL programs: how to reflect the temporal properties in MSVL programs;how to execute the multi paths existed in MSVL programs;the implementation of the specific statements in MSVL and the display of the program's model.Finally,this thesis introduces the usage of our MSVL modeling tool,and gives the model result for a classic problem,which checks the feasibility of the proposed framework.