基于模型检测的内存泄露静态测试方法  

Static Detection to Memory Leak Based on Model Checking

作　　者：付晓毓[1] 朱利[1] 顾伟[1] 

机构地区：[1]西安交通大学软件学院,陕西西安710049

出　　处：《微电子学与计算机》2010年第10期170-173,共4页Microelectronics & Computer

基　　金：国家自然科学基金项目(60673087);国家"八六三"计划项目(2003AAIZ2610)

摘　　要：在C等支持动态内存分配的语言中,指针的使用带来的内存泄露是导致系统性能降低的重要问题.针对现有处理方法的不足,文中设计了一种基于模型检测技术的内存泄露静态检测方法.该方法通过建立基于指针属性的内存泄露漏洞模型,将相应约束断言插桩进源代码,然后利用模型检测工具验证断言的可达性来判断内存泄露.实验结果表明,该方法是有效的和精确的.In C language that support dynamic memory operations,the usage of pointer brings about memory leak which is the key factor that causes system performance degradation.For the inadequacy of existing approaches,a method of static detection to memory leak based on model checking was proposed in this paper.By modeling memory leak vulnerabilities based on the attributes of a pointer,the method instrument the source code with corresponding constraint assertions,and then verify the reachability of these assertions by model checking tools.Experimental results show that the method is effective and accurate.

关 键 词：模型检测 内存泄露 代码插桩 静态测试 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]