6静态程序分析方法和工具的不足-四川大学.doc

本科生毕业论文（设计） 题 目 静态程序分析方法和工具 学 院 计算机学院 　 专 业 计算机科学与技术 学生姓名 高婉玲 　 学 号 1043041385 年级 2010 指导教师 洪玫 　 教务处制表 二ΟΟ四年五月三日 静态程序分析方法和工具 计算机科学与技术专业 学生：高婉玲 指导老师：洪玫 [摘要]这篇论文主要研究静态程序分析的方法和工具，以及静态程序分析工具在软件测试中的应用。论文采用系统化文献评价方法和文献计量分析方法，通过论文的收集、筛选、内容提取等过程，对大量论文的信息进行总结分析。通过文献管理工具Endnote、数据分析软件SPSS和文献分析工具RefViz，可统计分析论文数据库的基本信息，如年代分布、来源期刊和出版地区分布、作者分布、关键词和热点分析。通过阅读大量相关论文内容，静态程序分析方法大致可分为形式化验证（包括模型检测、符号执行和定理证明等）、抽象解释、程序切片和实验程序分析方法等；静态程序分析工具包括形式化验证工具、模型检测工具、抽象解释工具和定理证明工具等；论文举例说明静态程序分析工具在软件测试中的应用十分广泛；另外，论文还总结了静态分析方法和工具误报率太高、分析精度较低等不足，以及在未来的工作中静态分析和动态分析结合的研究趋势。 目录 静态程序分析方法和工具 2 1. 引言 3 1.1研究背景 3 1.2主要知识点 4 1.3研究意义和价值 4 1.4研究线路 5 2. 研究方法 5 2.1系统化文献评价方法 5 2.1.1研究问题 5 2.1.2数据来源 6 2.1.3筛选原则 6 2.1.4数据提取和分析 6 2.1.5完成报告 6 2.2文献分析框架、工具和分析过程 6 2.2.1文献分析框架 6 2.2.2工具介绍 7 2.2.3文献分析过程 8 3. 文献计量分析结果 8 3.1年代分布 8 3.2来源期刊和出版地区分布 9 3.3作者分布 9 3.4关键词和热点分析 11 4. 静态程序分析方法 12 4.1形式化验证（Formal Verification） 13 4.2模型检测（Model Checking） 13 4.3符号执行（Symbolic Execution） 14 4.4定理证明（Theorem Proving） 15 4.5抽象解释（Abstract?Interpretation） 15 4.6程序切片（Program Slicing） 15 4.7实验程序分析方法(Experimental Program Analysis) 16 4.8其他方法 16 4.9静态程序分析方法比较 17 5. 静态程序分析工具 17 5.1形式化验证工具 17 5.2模型检测工具 18 5.3定理证明工具 19 5.4抽象解释工具 19 5.5其他工具 20 6. 静态程序分析方法和工具的不足 20 7.工具在软件测试中的应用实例 21 7.1 SoftWare IMmunization (SWIM)在测试中的应用 21 7.2代码驱动的测试用例生成 22 7.3自动化错误定位工具在软件测试中的应用 22 7.4主流Java静态代码分析工具在软件测试中的应用 23 8. 未解决的问题和未来的工作 24 9. 参考文献 24 声明 28 致谢 29 译文 29 原文 29 引言 1.1研究背景 程序分析是计算机科学与技术领域的经典和核心内容,是以某种语言书写的程序为对象，对其内部的运作流程进行分析 根据程序是否需要运行，程序分析技术包括静态程序分析和动态分析技术。分析（Program Static Analysis）是在不运行代码的下，，。静态分析。动态分析是通过在真实或模拟环境中执行程序进行分析的方法，多用于性能测试、功能测试、内存泄漏测试等方面。动态分析包括插装等静态分析与动态分析 静态分析和动态分析基本过程[1]如图1： 图1：静态分析和动态分析基本过程图 1.3研究意义和价值 这篇论文先采用文献计量分析来统计分析与静态程序分析有关的论文的基本信息，用以展现进10年来静态程序分析的发展和热点。论文在文献基本信息分析后综述静态程序分析的方法和工具,同时举例描述静态程序分析工具在软件测试中的应用,总结静态程序分析的不足和未解决的问题，并展望静态程序分析技术未来的方向。静态程序分析的目标不是证明程序完全正确，而是作为动态测试的补充，在程序运行前尽可能多的发现隐含错误，提高程序的