随着计算机技术的发展,软硬件的正确性和可靠性已经成为使用方关注的一项重要指标,特别是在航空航天、军工控制系统中,这一点尤为明显。模型检测作为一种形式化验证技术,受到各个相关领域的青睐。模型检测的基本思想是对给定的系统进行建模,用时序逻辑公式表示待验证的系统性质,然后用验证器验证该系统模型是否满足给定的性质,如果不满足给定的性质,则给出反例路径。模型检测虽然有着自动化验证等优点,但是也受制于状态空间爆炸问题。为了缓解模型检测过程中出现的状态空间爆炸问题,目前提出了很多有效的方法,如基于偏序归约技术的偏序模型检测等。偏序模型检测器SPIN是由贝尔实验室开发的开源软件,它多用来检测分布式软件模型的正确性,并且它能以一种严格且自动化的形式进行验证。SPIN使用Promela语言对系统进行建模,用LTL公式描述系统模型的性质,然后将该性质的非转换成对应的Büchi自动机,最后由验证器自动执行验证过程,得出结果。但是LTL的表达能力不是完全正则的,有些性质并不能用LTL公式表示出来,因此需要用一种表达能力更强的时序逻辑来描述系统的性质。PPTL具有完全正则的表达能力,并且PPTL的可判定性也已经得到了证明,因此本文实现了基于SPIN的PPTL偏序模型检测器,并给出了该偏序模型检测器的验证实例。本文首先研究了PPTL公式到Büchi自动机的转换算法包括PPTL公式到带标记的范式图的转换、带标记的范式图到广义Büchi自动机的转换和广义Büchi自动机到Büchi自动机的转换。然后在SPIN的基础上增加了PPTL公式到NeverClaim形式的转换过程,实现了PPTL的偏序模型检测器。给出了PPTL公式到NeverClaim形式的转换过程的设计类图、主要函数以及各个模块的程序流程图,并用两个PPTL公式转换实例展示了该转换过程生成的带标记的范式图、Büchi自动机和NeverClaim形式。最后给出了基于密码协议的KDC协议的验证实例,用Promela语言对KDC协议进行建模,用PPTL公式描述该协议的性质,并利用该模型检测器检测出KDC协议中存在的攻击路径。