基于程序局部性引导的有界模型检测优化方法  

Locality-guided based optimization method for bounded model checker

作　　者：王舜 杜晔[1] 韩臻[1] 刘吉强[1] WANG Shun;DU Ye;HAN Zhen;LIU Jiqiang(Beijing Key Laboratory of Security and Privacy in Intelligent Transportation, Beijing Jiaotong University, Beijing 100044, China)

机构地区：[1]北京交通大学智能交通数据安全与隐私保护技术北京市重点实验室,北京100044

出　　处：《通信学报》2018年第3期181-190,共10页Journal on Communications

基　　金：北京高校青年英才计划基金资助项目(No.YETP0548);国家自然科学基金资助项目(No.61672092)~~

摘　　要：基于多种模型检测方法组合的复合检测方式是当前软件模型检测领域开展研究的热点之一。在当前的研究中,提高检测的规模和检测的对象复杂程度的关键在于如何有效处理抽象的扩张和收缩。证明通过对程序模式或验证信息的利用可以加快状态空间的探索速度。面向有界模型检测(BMC)加速方法展开研究,使用程序中额外的信息和知识对其处理以协助检测器删除冗余和无效的状态。在对程序局部性进行定义的基础上,对其加速性进行讨论,提出一种加速有界检测的方法和一种改进策略,对算法进行了详细描述,并通过实验验证了方法在检测效率和性能上的优越性。For software model checking,approaches that combine with different kind of verification methods are now under research.The key to improve scale and complexity of verifiable software is handling the method for abstraction widening and strengthening wisely and precisely.To archive that,using extra knowledge that extracted from programming pattern or learned through verifying procedure to help eliminate the redundant state has been proved effective.Definition of program locality was given.It took the important role in accelerating software verification,then the strategy was raised and an algorithm was implemented to take advantage of program locality.This method exploits the features of modern BMC(bounded model checker)and scales up the capability of its power in large scale and comprehensive software modules.

关 键 词：模型检测 BMC 软件检测 局部性 优化 

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