资源描述：
《advances in predicate abstraction》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。
1、ISSN1000-9825,CODENRUXUEWE-mail:jos@iscas.ac.cnJournalofSoftware,Vol.19,No.1,January2008,pp.27−38http://www.jos.org.cnDOI:10.3724/SP.J.1001.2008.00027Tel/Fax:+86-10-62562563©2008byJournalofSoftware.Allrightsreserved.∗谓词抽象技术研究+屈婉霞,李暾,郭阳,杨晓东(国防科学技术大学计算机学院,湖南长沙410073)
2、AdvancesinPredicateAbstraction+QUWan-Xia,LITun,GUOYang,YANGXiao-Dong(SchoolofComputer,NationalUniversityofDefenseTechnology,Changsha410073,China)+Correspondingauthor:Phn:+86-731-4573679,E-mail:wxqu2002@yahoo.com.cnQuWX,LiT,GuoY,YangXD.Advancesinpredicateabstraction
3、.JournalofSoftware,2008,19(1):27−38.http://www.jos.org.cn/1000-9825/19/27.htmAbstract:Withthegrowingincreaseinsoftware/hardwaresystemscaleandfunction,thefurtherdevelopmentandapplicationofmodelcheckinghasbeengreatlylimitedbystatespaceexplosion,whichbecomesthebottlen
4、eckofverifyinglargeindustrialdesigns.Predicateabstraction,asoneofthemosteffectivewaystoaddressstateexplosion,hasbeenfueledovertherecentyears.Thispaperpresentsasurveyofthelatestdevelopmentsinpredicateabstraction.Abasicalgorithmforpredicateabstractionisintroducedfirs
5、t,followedbycomparisonamongseveralsolvers.Emphasesareputoncounterexample-guidedabstractionrefinementandinterpolation-basedabstractionrefinement,includingtheprinciplesandimprovements.Thequalitiesofthenewpredicategenerationmethodsarealsoanalyzed.Finally,themajorchall
6、engesinmakingthistechnologymorepervasiveinindustrialdesignverificationdomainarenoted.Keywords:modelchecking;predicateabstraction;abstractionrefinement;counterexample;interpolation摘要:随着软、硬件系统规模和功能的不断扩充,状态空间爆炸问题严重影响了模型检验的进一步发展与应用,成为验证大规模系统的瓶颈.谓词抽象是解决状态空间爆炸的最有效方法之一,近年
7、来得到迅速发展.介绍了谓词抽象的基本算法并比较了不同的求解支持工具;重点分析了反例指导的抽象求精和基于插值的抽象求精原理;分析了产生新谓词的各种方法的优、缺点;最后指出了谓词抽象技术进一步发展所面临的挑战和发展方向.关键词:模型检验;谓词抽象;抽象求精;反例;插值中图法分类号:TP301文献标识码:A随着软硬件系统规模和功能的不断扩充,系统的正确性验证日益困难.目前,功能验证主要采用模拟和形式化验证方法.模拟方法是目前的主流验证方法,但由于它极大地依赖于模拟激励,因此很难保证验证的完备性.形式化验证方法是对模拟方法的重要补充
8、,它使用严格的数学推理来证明系统是否满足全部或部分规范(又称为系统属性),大体上可分为等价性检验、模型检验和定理证明3类.模型检验通过遍历状态空间自动地判断一个有限状态系统是否满足某些属性,在最坏情况下,状态空间的∗SupportedbytheNationalNaturalScienceF
