The Extension And Application Of The Modeling,Simulation And Verification Tool

This thesis mainly discusses the implementation principle, extension and some applications of the Modeling, Simulation and Verification Language(MSVL) tool. MSVL is a kind of temporal logic programming language. A software or hardware system can be simulated, modelled and verified using MSVL in this tool we have developed.First of all, the basic logic, projection temporal logic(PTL) are presented, including syntax and semantics. Then, the Modeling, Simulation and Verification Language based on PTL are introduced. Basic statements in MSVL are given.The basic approach, including normal form, normal form graph and a unified model checking approach with PTL, are presented firstly. After that, the functions and structure of the MSVL tool are discussed and each of its modules is explained in detail. Then, the extension in Object-Oriented programming of the MSVL tool are introduced, referring basic theroies, detailed implementation and an analysis of an Object-Oriented MSVL example.Subsequently, concerned with describing some special concurrent systems, this thesis shows an extension of Cylinder Computation in MSVL tool. Similarly, the basic approach, tool implementation are presented. Meanwhile, an application is used to explain the new Cylinder Computation.Finally, this thesis points how to implement the Labelled unified model checking approach with PTL. First it reviews the unified model checking approach with PTL.Then it gives the concrete steps to implement the Labelled algorithm in MSVL tool. This part ends with two infinite interval model checking example.