Research And Implement Of The Asynchronous Communication In MSVL

With the rapid development of computer technology and Internet, a variety ofcomputer software and hardware systems have widely infiltrated into human life andproduction. However, how to ensure that the computer systems run in strict accordancewith the designing has become one of the computer-related research topics. As aformal method, temporal logic is widly used in system modeling and verification.MSVL (Modeling, Simulation and Verification Language) is a kind of temporallogic programming language based on PTL (Projection Temporal Logic). A computersoftware or hardware system can be simulated, modeled and verified using MSVL.This thesis mainly discusses the implementation of asynchronous communicationtechniques in MSVL. First, PTL and MSVL are presented, including syntax andsemantics. Moreover, the functions and structure of the MSVL interpreter are discussedbriefly. After that, asynchronous communication is formalized by introducing theprocess, channel and communication commands. Process is used to model thecomponents of a system. Channel is a buffer between different components formessage storage. Communication commands are executed to finish the messagepassing. In addition, the implement of asynchronous communication in MSVLinterpreter is given. Finally, three examples are demonstrated to test the works on theimplement of asynchronous communication.