基于最弱前置条件的程序正确性分析

摘要：

随着软件的不断更新迭代,软件正确性检测的必要性愈加凸显,软件正确性检测的处理时间直接决定软件的维护成本.动态测试的断言编写和静态分析的符号执行均针对程序正确性进行优化完善,但分析结果易出现路径缺失甚至错误无法识别等问题.现有验证方法在路径扩展时易生成较多无用路径,且针对性不强,因此有必要研究一种更为可靠的方案.本文采用最弱前置条件对软件可行性加以分析,对程序执行语义正确建模,使用程序切片技术预处理程序代码,并根据层级结构存储节点及其子程序.实验结果表明,该方法可以有效减小静态分析对程序状态抽象操作带来的验证精度损耗,且能够遍历求解出程序的所有可能路径,并通过分组标出条件表达式的结论真假值,以此验证路径正确性,同时可对高复杂的程序代码进行有效的正确性分析.

关键词：程序正确性、最弱前置条件、静态分析、路径扩展、程序切片技术

所属期刊栏目：29

资助基金：国家自然基金61402333,61272450;天津市自然科学基金18JCZDJC30700 和赛尔网络下一代互联网技术创新项目NGII20160121

在线出版日期：2019-07-18（万方平台首次上网日期，不代表论文的发表时间）

页数：共8页

页码：556-563