模型检测是一种形式化验证方法，目前已经得到了广泛的发展和应用。本文给出的是一种基于命题投影时序逻辑（Propositional Projection Temporal Logic,PPTL）的模型检测器的改进和应用，该模型检测器是在SPIN的基础上添加和修改部分模块实现的。PPTL模型检测器用Promela语言描述系统模型，用PPTL公式描述待验证的系统性质。由于PPTL在SPIN中无法识别，因此需要将PPTL公式转换为SPIN可接收的Never Claim，才能够在SPIN基础之上实现PPTL模型检测。本文主要研究PPTL公式到Never Claim的改进转换算法。首先，简单介绍了PPTL的语法、语义以及一些等价关系和逻辑法则等，还给出了模型检测技术的原理和发展，并重点介绍了模型检测器SPIN的相关内容，然后详细介绍了PPTL公式向Never Claim转换的过程：PPTL公式→范式（Normal Form, NF）→带标记的范式图（Labeled Normal Form Graph, LNFG）→Never Claim，并给出了实现每一步的算法，其中改进的算法是LNFG和Never Claim的生成算法。最后本文通过著名的German-2004协议和Russian Cards problem五人问题两个实例说明了改进后的模型检测器的实际工作过程。