Research And Implementation Of MSVL Compiler And Integrated Development Environment Based On Linux

With the extensive application of computer systems,the correctness and reliability of software systems are crucial to human safety in production and life.With the increase in the scale and complexity of software systems,traditional software testing methods can no longer meet the needs of ensuring software reliability.After decades of development,formal verification has become an important method for ensuring software reliability.Among the formal verification methods,the method of verifying the software system by using temporal logic has been widely used.The temporal logical programming language MSVL was developed from Projection Temporal Logic and can be used for modeling,simulation,and verification of hardware and software systems.This paper mainly studies the implementation of MSVL compiler and MSVL Integrated Development Environment(IDE)on Linux.The implementation of MSVL compiler is significantly different from the conventional compilers for imperative programs because the execution of MSVL is different from conventional ones.MSVL compiler was developed based on the LLVM framework and the LLVM Intermediate Representation is selected as the intermediate code.The translation of MSVL statements into intermediate code is the core content of this paper,and it is also a difficult point in the implementation of MSVL compiler.This paper first introduces the design and implementation of the MSVL compiler's framework,and then the conversion methods from the MSVL statement to the LLVM code representation.The implementation of MSVL IDE is another section of this paper.The implementation of MSVL IDE is based on the Eclipse platform and provides a graphical user interface(GUI)for the MSVL tools on the Linux platform.Finally,the method and effect of using the MSVL compiler through the command terminal and MSVL IDE are shown.