软件学报

作者：王笑爽，周志德，李晓晨，江贺，任志磊

单位：王笑爽，大连理工大学 软件学院, 辽宁 大连 11602411,周志德，大连理工大学 软件学院, 辽宁 大连 11602402,李晓晨，大连理工大学 软件学院, 辽宁 大连 11602403,江贺，大连理工大学 软件学院, 辽宁 大连 11602404,任志磊，大连理工大学 软件学院, 辽宁 大连 116024;高安全系统的软件开发与验证技术工业和信息化部重点实验室(南京航空航天大学), 江苏 南京 21001605

关键词：SMT求解器;缺陷定位;覆盖频谱;历史频谱

基金：南京航空航天大学科研基地创新(理工类)项目(NJ2020022); 国家自然科学基金(62072068, 62032004); 国家重点研发计划(2018YFB1003900)

SMT求解器作为重要的基础软件, 其存在的缺陷可能会导致依赖于它的软件功能失效, 甚至带来安全事故. 然而, 修复SMT求解器缺陷是一个十分耗时的任务, 因为开发者需要花费大量的时间和精力来理解并找到缺陷的根本原因. 虽然已有许多软件缺陷定位方面的研究, 但尚未有系统的工作研究如何自动定位SMT求解器缺陷. 因此, 提出一种基于多源频谱的SMT求解器缺陷定位方法SMTLOC. 首先, 对于给定的SMT求解器缺陷, SMTLOC提出一种枚举算法, 用以对触发该缺陷的公式进行变异, 从而生成一组不触发缺陷, 但与触发缺陷的公式具有相似执行路径的证人公式. 然后, SMTLOC根据证人公式的执行路径以及SMT求解器的源码信息, 提出一种融合覆盖频谱和历史频谱的文件可疑度计算方法, 从而定位可能存在缺陷的文件. 为了验证SMTLOC的有效性, 收集60个SMT求解器缺陷. 实验结果表明, SMTLOC的缺陷定位效果明显优于传统的频谱缺陷定位方法, SMTLOC可以将46.67%的缺陷定位在TOP-5的文件内, 定位效果提升了133.33%.

来源：2024年第7期

《软件学报》期刊编辑部

查看软件学报杂志2024年第7期