软件学报

作者：苏杰，杨祖超，田聪，段振华

单位：苏杰，西安电子科技大学 计算机理论与技术研究所, 陕西 西安 710071;综合业务网理论及关键技术国家重点实验室(西安电子科技大学), 陕西 西安 71007111,杨祖超，西安电子科技大学 计算机理论与技术研究所, 陕西 西安 710071;综合业务网理论及关键技术国家重点实验室(西安电子科技大学), 陕西 西安 71007102,田聪，西安电子科技大学 计算机理论与技术研究所, 陕西 西安 710071;综合业务网理论及关键技术国家重点实验室(西安电子科技大学), 陕西 西安 71007103,段振华，西安电子科技大学 计算机理论与技术研究所, 陕西 西安 710071;综合业务网理论及关键技术国家重点实验室(西安电子科技大学), 陕西 西安 71007104

关键词：约束依赖图;偏序约简;并发程序;模型检测;工具

基金：国家自然科学基金（62192730，62192734，61732013，62172322）；科技创新2030——“新一代人工智能”重大项目（2018AAA0103202）

模型检测是一种基于状态空间搜索的自动化验证方法，可以有效地提升程序的质量.然而，由于并发程序中线程调度的不确定性以及数据同步的复杂性，对该类程序验证时存在更为严重的状态空间爆炸问题.目前，大多采用基于独立性分析的偏序约简技术缩小并发程序探索空间.针对粗糙的独立性分析会显著增加需探索的等价类路径问题，开发了一款可细化线程迁移依赖性分析的并发程序模型检测工具CDG4CPV.首先，构造了待验证可达性性质对应的规约自动机；随后，根据线程迁移边的类型和共享变量访问信息构建约束依赖图；最后，利用约束依赖图剪裁控制流图在展开过程中的独立可执行分支.在SV-COMP 2022竞赛的并发程序数据集上进行了对比实验，并对工具的效率进行比较分析.实验结果表明，该工具可以有效地提升并发程序模型检测的效率.特别是，与基于BDD的程序分析算法相比，该工具可使探索状态数目平均减少91.38%，使时间和空间开销分别平均降低86.25%和69.80%.

来源：2023年第7期

《软件学报》期刊编辑部

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