本发明是一种基于SAT的命题投影时序逻辑限界模型检测方法，步骤是：用Kripke结构描述待验证系统模型M；用PPTL公式描述性质P；设定限界k；将PPTL限界模型检测转换为SAT问题；对SAT问题求解：有解，系统M不满足性质P，给出反例，无解，系统M有界满足性质P，增大k值，进入下一个检测周期，直到k值足够大且在每个限界模型检测周期内待验证系统M都有界满足性质P。本发明使用PPTL描述系统性质，解决了CTL和LTL表达能力有限的问题，并通过限制搜索长度减少搜索状态数，缓解了状态空间爆炸，融合了PPTL和BMC各自的优点，使系统复杂性质的验证更方便有效。本发明适用于软硬件系统以及通信协议的形式化验证。