基于SMT的TECTL性质的限界模型检测方法  

Bounded model checking of TECTL properties based on SMT

作　　者：徐亮[1] 刘宏[2] 

机构地区：[1]湖南师范大学数学与计算机科学学院,湖南长沙410081 [2]高性能计算与随机信息处理省部共建教育部重点实验室,湖南长沙410081

出　　处：《计算机工程与科学》2013年第10期166-171,共6页Computer Engineering & Science

基　　金：国家自然科学基金资助项目(60903168);湖南省教育厅科学研究项目(13C527);湖南省科技计划资助项目(2012FJ6012);长沙市科技计划资助项目(K1109020-11);湖南省重点学科建设资助项目(湘教发[2011]76号)

摘　　要：近些年来,基于SMT的限界模型检测方法作为基于SAT的限界模型检测方法的一种改进,在对实时系统的检测上已经得到了一定发展。一直以来,限界模型检测多被用于检验存在性性质,而很少用于验证全局性性质,原因之一就是该方法受界限的限制,很难实现对全局性性质的有效编码。为此,通过对传统限界模型检测中的编码方式进行相应改变,在一定程度上解决了这一问题。同时,结合SMT,实现了对实时系统中某些全局性性质的验证。实验表明该方法比已有的方法效率更高。Satisfiability Modulo Theories （SMT）-based bounded model checking （BMC） has been considered as an improved technique to SAT-based bounded model checking in recent years.Bounded model checking has often been used to check existential properties,but rarely used to verify global properties,and one of the reasons is that this method is hard to encode the global properties as its＇ restricted by the bound.Therefore,In order to verify the global properties,the encodings in traditional bounded model checking should be changed.Combining with SMT,some global properties can be verified in real time systems.Experiments demonstrate the method is more efficient than existing methods.

关 键 词：限界模型检测 可满足性模理论 全局性性质 实时系统 验证 

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]