随着计算机和互联网技术的快速发展，各种计算机软、硬件系统已广泛渗透到人类生产和生活中，然而如何保证计算机系统严格按照人类设计的方式工作已成为当前计算机相关研究课题之一。时序逻辑作为一种形式化方法已广泛应用于系统的建模与验证中。MSVL (Modeling, Simulation and Verification Language)是一种基于投影时序逻辑PTL (Projection Temporal Logic)的时序逻辑语言，它可用于对计算机软、硬件系统进行建模、仿真和验证。本文实现了MSVL的异步通信方法，以实现MSVL对异步并发系统的建模与验证。文中首先介绍了PTL和MSVL的语法和语义，并讨论了MSVL解释器的实现原理及功能，接着形式化定义了进程，通道以及通信命令的语法和语义，进程用于对并发系统中的组件进行建模，通道作为不同组件之间通信的消息缓冲，进程执行通信命令实现不同组件之间的消息传递，此外文中还给出了MSVL解释器中异步通信的实现过程，最后通过三个具体实例详细分析了MSVL异步通信方法的可行性。