目前软件工业界面临着产品功能越来越复杂和推出产品周期越来越短的双重压力。软件工程的一个主要目标就是在复杂性增加的情况下仍能构造正确可靠的系统。为了达到上述目标,形式化方法在软件开发中得到了广泛的应用,特别是模型检查技术。本文提出了一种基于SPIN的命题投影时序逻辑的模型检查方法。在此方法中,系统的性质用命题投影时序逻辑公式来描述,随后这个公式被转换为其永非断言;然后系统模型用Buchi自动机来刻画;最后通过SPIN完成模型检查,即检查系统是否满足期望的性质。为了实现这一目的,文中设计并实现了命题投影时序逻辑公式的解释转换器,以便将命题投影时序逻辑公式自动转换为Promela形式的永非断言。该转换器首先将待验证的命题投影时序逻辑公式转换为其正则式以及正则图,然后通过正则图可以得到所需的永非断言。将该转换器与模型检查器SPIN相结合,使用命题投影时序逻辑公式来在SPIN中描述系统的性质,这样基于命题投影时序逻辑的模型检查就能在SPIN中完成。