随着计算机和互联网技术的快速发展，各种软、硬件系统已经广泛渗透到人类生产和生活中，如何保证计算机系统严格按照人类设计的方式进行工作已经成为当前计算机相关研究课题之一。采用形式化方法来描述软硬件系统，能够有效地减少系统设计中的错误，提高设计的可靠性。时序逻辑作为一种形式化方法已被广泛的应用于系统的仿真和验证中。建模仿真和验证语言(Modeling, Simulation and Verification Language，MSVL)是一种基于投影时序逻辑(Projection Temporal Logic，PTL)的时序逻辑程序设计语言，它可以用于对计算机软硬件系统进行建模、仿真和验证。本文主要讨论Linux环境下基于MSVL的仿真和验证。文中首先介绍了PTL和MSVL的语法和语义，并讨论了MSVL解释器的实现原理和功能，接着介绍了MSVL对系统进行仿真和验证的原理，然后基于系统层次化设计理论详细介绍了MSVL对系统的形式化描述方法，最后给出了一个用MSVL对CTCS-3列控系统进行形式化描述的实例，借助解释器MSV实现了对CTCS-3系统的仿真和验证，并给出了仿真和验证的结果。实例结果表明，此方法可以有效地检测系统设计上的缺陷。