基于SAT工具的限界模型检测归约方法  

Reduction Method of Bounded Model Checking Based on SAT Tool

作　　者：喻超[1] 毋国庆[2] 

机构地区：[1]成都东软信息技术学院科研管理部,成都611844 [2]武汉大学计算机学院,武汉430072

出　　处：《计算机工程》2010年第17期60-62,共3页Computer Engineering

摘　　要：限界模型检测主要对路径上的属性进行检测,基于此给出一种编码方法,将LTL公式在路径上展开,从而将限界模型检测转换为命题逻辑的可满足性问题,使用SAT求解工具来完成模型检测过程。阐述归约过程的正确性与完全性,通过一个具体例子证明了该方法的有效性。Bounded model checking is mainly used to detect the property in the path. This paper proposes an encode method which is used to extend the LTL formulas in path, then bounded model checking can be reduced to the problem of whether the propositional logic formula is satisfiable or not, and SAT checking tool can be used to complete the process. The reducing process is proved to be correct and complete. An specific example is given to show the validity of the method.

关 键 词：模型检测 形式化验证 归约 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]