摘要
随着软件的不断更新迭代,软件正确性检测的必要性愈加凸显,软件正确性检测的处理时间直接决定软件的维护成本。动态测试的断言编写和静态分析的符号执行均针对程序正确性进行优化完善,但分析结果易出现路径缺失甚至错误无法识别等问题。现有验证方法在路径扩展时易生成较多无用路径,且针对性不强,因此有必要研究一种更为可靠的方案。本文采用最弱前置条件对软件可行性加以分析,对程序执行语义正确建模,使用程序切片技术预处理程序代码,并根据层级结构存储节点及其子程序。实验结果表明,该方法可以有效减小静态分析对程序状态抽象操作带来的验证精度损耗,且能够遍历求解出程序的所有可能路径,并通过分组标出条件表达式的结论真假值,以此验证路径正确性,同时可对高复杂的程序代码进行有效的正确性分析。
With the constant iteration of software, the necessity of software correctness detection accumulatively highlights and the time of software correctness processing detection directly determines the maintenance cost. The assertion of dynamic analysis and the symbolic execution of static analysis are optimized for the correctness of program, but the analysis results are prone to problems such as missing paths or unrecognizing errors. The existing verification methods easily generate more useless paths when the paths are extended, and the pertinence is weak, so it is neccesary to study a more reliable solution. The weakest preconditions are used to analyze the software feasibility. Then model program execution semantics correctly and preprocess program codes by program slicing technology. In addition, the nodes and their subroutines are stored according to the hierarchical structure. The experiment results show that the proposed method can effectively reduce the loss of verification accuracy caused by static analysis on the program state for abstraction operation, and traverse all possible paths of the program. Then by grouping and marking the true and false values of the conditional expressions the method can verify path correctness and analyze efficiently correctness of highly complex program codes.
作者
郭莎莎
侯春燕
王劲松
Guo Shasha;Hou Chunyan;Wang Jinsong(School of Computer Science and Engineering, Tianjin University of Technology, Tianjin 300384)
出处
《高技术通讯》
EI
CAS
北大核心
2019年第6期556-563,共8页
Chinese High Technology Letters
基金
国家自然基金(61402333,61272450)
天津市自然科学基金(18JCZDJC30700)
赛尔网络下一代互联网技术创新项目(NGII20160121)资助
关键词
程序正确性
最弱前置条件
静态分析
路径扩展
程序切片技术
program correctness
the weakest precondition
static analysis
path extension
program slicing technology
