● 摘要
不变式的动态发现技术是一种新兴的程序动态分析技术，它通过对程序动态执行状态的分析逆向地提取不变式。动态发现不变式的思想最初是由MIT的Michael D.Ernst于1999年提出的，之后相关研究日益丰富。其主要思想是：首先，从源程序中提取程序点上变量的动静态信息；然后，分析变量的静态信息，依据系统给定的不变式规则实例化出所有潜在不变式；最后，依据变量的动态信息（变量值），检测并剔除不成立的关系式。程序不变式动态发现技术的研究具有重要的价值和潜在的应用前景，可以应用于辅助程序理解、程序版本验证、故障定位及软件重构等领域。 本课题在学习不变式动态分析的相关理论和调研国外相关研究成果的基础上，仔细分析了动态不变式发现过程中的各个关键技术，研究并提出了自己的技术方案，并实现了一个适用于C/C++程序的不变式自动发现工具。 本文的研究内容包括：在变量信息提取方面，提出了扩展解释器CINT提取变量信息的方式；在不变式描述方面，设计了内置的不变式规则五十余条，并提出以动态插装的方式支持用户自定义潜在不变式；在不变式的检测算法方面，结合了传统的多遍递增检测算法和自底向上检测算法的优点，提出了多遍自底向上检测算法；在不变式的种类方面，除了支持现有工具已有的函数前置不变式和后置不变式，还支持面向对象软件的类不变式的动态提取。 本文介绍了不变式动态发现技术的研究现状，阐述了不变式发现技术的相关研究基础。在此基础上，详细讨论了本课题提出的动态发现不变式过程中的若干关键技术，并详细介绍了不变式自动发现工具的设计与实现。最后，通过实例分析展示了工具所发现的不变式，并给出与其他相关工具比较的结果。关键词：程序不变式，程序点，不变式规则，动态分析，测试用例
相关内容
相关标签