随着计算机技术的飞速发展,世界各国由于软件错误带来的灾难数不胜数。软件系统的正确性、可靠性、安全性对人们的日常生活和国防建设都非常重要。模型检测作为一种形式化的验证方法,广泛地应用于软硬件系统、嵌入式系统、通信协议系统的验证。但是,模型检测中也存在一些缺点,首先,随着模型规模的增大,模型中状态数呈指数性增加,出现了严重的状态空间爆炸问题。其次,目前常用的时序逻辑的语言表达能力有限。本文的研究目的正是基于这两点。面对上述问题,本文首先研究命题投影时序逻辑(Propositional Projection Temporal Logic,PPTL)理论知识。然后,研究模型检测的基本方法和理论。最后,设计并开发多策略的PPTL模型检测工具集PPTLMC。本文使用PPTL描述待验证的规范,因为PPTL的表达能力是完全正则的,不仅可以验证用LTL和CTL描述的性质,而且还能够验证LTL和CTL不能描述的性质。特别地,可以验证区间相关以及周期性重复的性质。本文主要贡献如下:(1)本文设计并实现了PPTL符号模型检测算法,该算法首先将PPTL公式取非并转换为Büchi自动机,然后转换为SMV程序,最后通过和系统模型的结合判空来判断系统是否满足该性质。(2)本文研究并实现了多策略的PPTL模型检测工具集PPTLMC,其中不仅包括PPTL转换为范式、PPTL转换为带标记的范式图、PPTL转换为Büchi自动机和PPTL可满足性判断工具,而且集成了PPTL符号化模型检测工具、PPTL限界模型检测工具、PPTL偏序模型检测工具和PPTL Petri网模型检测工具。(3)随着移动互联网的发展,设计一个基于Web的PPTLMC工具是有意义的,本文设计并开发了基于Web的PPTLMC工具。(4)本文通过“摆渡者问题”和“AB(交换比特)协议”实例来验证PPTLMC工具集中的各个模型检测工具的正确性和实用性。