基于抽象解释理论的程序循环边界分析

摘要

随着计算机科学的快速发展和计算机技术广泛应用，计算机软件能否正确运行，成为人们关注的焦点。特别是在一些重要的应用领域，对程序正确性的要求一方面要求程序的运行能够产生正确的运行结果。因为程序运行结果的细微的错误很有可能会带来重大是安全事故。另一方方面，还要对程序的执行时间有一定的要求。在一些安全关键领域的应用中，一旦程序无法在指定的时间范围内完成应有的工作，将会带来重大的财产损失和人员的伤亡。因此，对程序执行时间的分析成为一个重要的研究课题。 对程序执行时间的分析首先要对程序独立于硬件环境的执行过程进行分析。在程序的运行过程中，循环结构作为程序三种基本结构中最复杂的一种，循环的迭代次数对程序的执行时间会产生重要的影响。本文就是针对程序执行过程中循环结构的迭代次数进行分析。论文的主要内容如下： （1）通过构建程序的控制流程图和数据依赖图来获取程序的数据依赖和控制依赖，构建程序依赖图。根据程序的依赖关系，通过去除程序依赖图中与程序执行过程无关的节点，得到简化后的程序依赖图，来指导程序切片。 （2）在区间抽象域上构建程序变量和程序计算的抽象表达。结合程序依赖图构建过程中获取的程序循环变量的约束信息，通过改进已有的计算程序循环边界的方法，获取较为精确的程序循环边界。 （3）构建程序循环边界分析框架。对案例程序进行循环边界进行分析计算，并且使用形式化的分析验证工具Frama-C的值分析插件对计算得到的程序循环边界进行验证。证明本文提出的分析方法的有效性。

目录

第一个书签之前

摘 要

目 录