基于抽象域和数值熵协同的数值程序分析

计算机工程与应用 ›› 2015, Vol. 51 ›› Issue (6): 55-58.

基于抽象域和数值熵协同的数值程序分析

马国富1，王正谦2，刘久富2

1.安阳工学院计算机科学与信息工程学院，河南安阳 455000
2.南京航空航天大学自动化学院，南京 210016

出版日期:2015-03-15 发布日期:2015-03-13

Value range analysis based on abstract domain and value entropy

MA Guofu1, WANG Zhengqian2, LIU Jiufu2

1.School of Computer Science and Information Engineering, Anyang Institute of Technology, Anyang, Henan 455000, China
2.College of Automation Engineering, Nanjing University of Aeronautics and Astronautics, Nanjing 210016, China

Online:2015-03-15 Published:2015-03-13

摘要/Abstract

摘要： 在软件日益丰富的信息时代，程序的正确性验证问题需要深入地研究。提出了基于抽象解释和数值熵协同的数值程序正确性分析方法。利用抽象解释理论框架对数值程序进行抽象解释分析，提取不变量的抽象域区间；在抽象域区间上进行数值熵运算；运行程序获取数值变量的实际取值，计算数值熵；将抽象域区间数值熵和实际数值熵信息进行对比分析，准确地判断程序的正确性等性质。单纯的抽象解释分析只可以近似得到数值变量的取值范围，而引入数值熵算法，在取值范围的基础上对程序静态分析的准确性进一步检验，同时也做到了对程序的正确性验证。通过C语言程序实例，对抽象解释基础上的熵值分析方法进行了验证，证明了该分析方法的可行性和正确性。

关键词: 数值程序分析, 正确性, 抽象解释, 数值信息熵

Abstract: In the information age, software is highly dependent, thus the correctness of the program validation issues need to be further studied. This paper introduces the value range analysis method based on abstract interpretation and value information entropy. The value program is analyzed by the abstract interpretation which is an important method of the static analysis, to obtain the abstract interpretation domain. Then it calculates the value information entropy, and runs the program to get the real values, in order to calculate the entropy. It compares the domain’s entropy with the values’ entropy, to accurately judge the correctness of the program, etc. The abstract interpretation analysis can only acquire the scope of variables, by introducing the value information entropy, this paper can make further inspection of the program static analysis based on the value range, and also verifies the correctness of the program. Through validating this method with C program, it verifies the practicality and correctness of this method.

Key words: value range analysis, validity, abstract interpretation, value information entropy

马国富1，王正谦2，刘久富2. 基于抽象域和数值熵协同的数值程序分析[J]. 计算机工程与应用, 2015, 51(6): 55-58.

MA Guofu1, WANG Zhengqian2, LIU Jiufu2. Value range analysis based on abstract domain and value entropy[J]. Computer Engineering and Applications, 2015, 51(6): 55-58.

[1]	汤莉1，2，赵政2，宫秀军2，3. 基于PAC-Bayes边界理论的SVM模型选择方法[J]. 计算机工程与应用, 2015, 51(6): 27-32.
[2]	张锦1，2，刘曼霞2，赵二群2，柳军飞3. 基于XYZ/SE的软件部分正确性验证[J]. 计算机工程与应用, 2015, 51(14): 46-50.
[3]	谢国珍，马晓星. C语言程序动态更新中的逻辑正确性[J]. 计算机工程与应用, 2013, 49(14): 39-44.
[4]	马艳芳1，2，陈亮3. 基于ε-互模拟的软件近似正确性模型[J]. 计算机工程与应用, 2013, 49(11): 15-19.
[5]	杨波^1，2，张明义³，谢刚⁴. 抽象解释理论框架及其应用[J]. 计算机工程与应用, 2010, 46(8): 16-20.
[6]	李伟刚¹,李俊亭². 过程实例跃迁正确性判定准则研究[J]. 计算机工程与应用, 2007, 43(36): 7-9.
[7]	胡金柱,焦金丹,胡燕,鲁志兵. 基于petri网的电子政务工作流模型研究[J]. 计算机工程与应用, 2007, 43(2期): 199-199.
[8]	陈卫东,张维明. 数据质量模型及选择运算中的质量传播研究[J]. 计算机工程与应用, 2007, 43(27): 1-3.