公开(公告)号：CN102663191B

公开(公告)日：2014-07-23

申请号：CN201210102064.3

申请日：2012-04-09

Applicant: 西安电子科技大学

Inventor： 段振华 ,  何佳 ,  田聪 ,  王小兵

IPC: G06F17/50

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

公开(公告)号：CN102663191A

公开(公告)日：2012-09-12

申请号：CN201210102064.3

申请日：2012-04-09

Applicant: 西安电子科技大学

Inventor： 段振华 ,  何佳 ,  田聪 ,  王小兵

IPC: G06F17/50

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