基于路径约束求解的多目标状态激励生成方法  

Test Generation for Multiple Target States Using Path Constraint Solving

作　　者：周艳红[1,2] 王天成[1,2] 李华伟[1] 吕涛[1] 李晓维[1] 

机构地区：[1]中国科学院计算技术研究所计算机体系结构国家重点实验室,北京100190 [2]中国科学院大学,北京100049

出　　处：《计算机学报》2016年第9期1829-1842,共14页Chinese Journal of Computers

基　　金：国家自然科学基金(61432017;61176040);国家"九七三"重点基础研究发展规划项目基金(2011CB302501)资助~~

摘　　要：该文提出了一种针对多个难达目标状态的激励生成方法,该方法基于抽象引导的半形式化方法框架.采用一个评估函数对候选状态进行评价,该评估函数综合考虑了从一个状态到不同目标状态的全局抽象距离信息,评价出从各个状态到达某个目标状态或者同时到达多个目标状态的潜能,并以此指导模拟过程直到最终搜索到一条能同时覆盖多个目标状态的状态序列.此外,该文采用了基于路径约束求解的激励生成方式,这种方式结合了具体模拟和符号模拟技术,符号模拟沿着具体执行路径提取分支条件构成路径约束,通过约束条件的翻转与求解能够有效地产生输入向量,以一种较均衡的模式遍历设计的状态空间,帮助验证快速覆盖到目标.实验结果表明,该文方法能够有效地同时验证设计中的多个目标状态.In this paper, we propose a test generation method to cover multiple hard-to-reach states, which operates in an abstraction-guided simulation framework. An evaluation function, which considers the global abstract distance information for one state to different target states, is used to evaluate the potentiality of each candidate next state to targets and guide the simulation processes to cover multiple target states. In addition, a path constraint solving based test generation method which combines concrete simulation and symbolic simulation is used. Symbolic simulation walks in the design following the concrete path and extracts the corresponding symbolic expressions of the branch conditions in the path as path constraints. The test generation engine can generate valid input vectors through constraint mutation and solving, and it helps to search state in the design state space in a balanced manner. Experimental results show that our approach is effective in covering multiple target states.

关 键 词：激励生成 难达状态 抽象引导模拟 路径约束求解 

分 类 号：TP393[自动化与计算机技术—计算机应用技术]