本文主要讨论基于投影时序逻辑PTL(Projection Temporal Logic)的MSVL(Modeling, Simulation and Verification Language)建模、仿真与验证软件的实现原理,扩展及应用,MSVL是一种时序逻辑程序设计语言,它是PTL的可执行子集,我们可以采用MSVL语言描述软、硬件系统,并对系统进行建模、仿真和自动化性质验证。文中首先介绍了PTL,并给出了实现MSVL建模、仿真及验证软件的基本方法,还详细说明了该软件的功能、基本框架以及各个模块的作用,然后,本文说明了对该软件进行的面向对象扩展,包括基本理论,具体实现以及简单的例子分析,接着,文中又给出了对MSVL建模、仿真与验证软件在柱面计算方面的扩充,同样,介绍了其实现的基本理论以及具体方法,并给出一个详细的例子,最后,本文介绍了如何实现加标记的PTL统一模型检测算法,回顾了PTL统一模型检测算法的实现步骤,给出了加标记的PTL统一模型检测算法及其在该软件中的实现,并给出了加标记的PTL统一模型检测算法验证无穷区间模型的例子。