基于模型检查的C程序分析技术研究

摘要

软件测试是为了发现错误而执行程序的过程,是保证软件质量的重要手段,因而成为软件生命周期中的重要阶段。在已有的测试工具中,源代码测试工具有着重要的应用。模型检查则是一种遍历系统所有可能执行路径的自动验证技术。最早由E.M.Clarke和E.A.Emerson在1981年提出,主要是米验证有穷状态并发系统的命题性质。它通常采用状态空间搜索的方法来检查一个给定的计算模型(程序)是否满足某个特定性质。在基于模型检查的软件代码分析和可靠性验证方面,国外少数大学和研究机构已经取得了一定的进展。目前仍需要解决和改善的问题主要集中在效率和准确性两个方面。
　　 本文主要讨论和分析了程序模型建立、模型检查和模型精化等方面的研究现状。针对软件单元测试和系统整合测试等阶段遇到的程序接口调用问题,给出了一个具体的方案。本文提出了多种策略尽可能满足用户对效率和准确性方面的不同需求,同时详细探讨了基于模型检查的程序测试框架中各个阶段使用的技术和算法,并于最后描述了基于模型检查的程序接口调用分析测试系统的设计与具体实现。通过本文给出的程序测试系统,可以帮助软件开发人员和测试人员软件在接口调用等方面是否存在错误和缺陷,检测源程序是否会出现因为接口调用所引起的内存泄漏和系统安全漏洞等问题,进而提高软件的可靠性和质量。

目录

文摘

英文文摘

第一章 绪论

1.1 选题依据

1.1 软件质量保证的目标与意义

1.2 研究现状

1.3 主要工作

1.5 论文结构

第二章 模型检查

2.1 简介

2.2 时序逻辑

2.3 基于自动机的模型检查方法

2.4 符号模型检查方法

2.4.1 基于二叉决策图的符号模型检查

2.4.2 基于命题可满足性问题的有界限模型检查

2.5 模型的抽象

第三章 基于模型检查的C语言代码测试

3.1 测试的基本概念

3.1.1 静态测试和动态测试

3.1.2 软件测试的步骤

3.2 程序接口调用的主要问题

3.3 基本框架

3.4 程序测试的策略

第四章 基于模型检查的代码测试

4.1 简单规范描述语言SSDL

4.1.1 简单规范描述语言的定义

4.1.2 简单规范描述语言的转换

4.2 C程序代码的模型建立

4.2.1 最弱前提断言

4.2.2 程序转换

4.2.3 C语言程序抽象

4.3 程序模型检查

4.4 程序模型精化

第五章 系统设计与实现

5.1 系统总体结构

5.2 C程序分析子系统的设计

5.2.1 信息库组织

5.2.2 C程序分析子系统的实现

5.3 C程序模型检查系统的设计

5.3.1 程序模型检查子系统的主要数据结构

5.3.2 程序模型检查子系统的结构组织

5.4 用户界面

第六章 结束语

致谢

参考文献