一种基于软件源代码级的验证技术研究

摘要

信息技术在现代生产生活各方面的应用越来越广泛，作为信息技术核心支撑的软件系统也变得越来越重要，其应用正在逐步渗透到社会的各个领域中去。时至今日，现在各行各业中的应用已经很难离开软件而独立运作了。软件系统已经成为了与我们的工作、生活密不可分的重要部分。软件系统的可靠与否，直接影响着人们的生产生活。在这个背景下，人们对软件系统的可靠性提出了越来越高的要求。
　　软件系统中最重要的实体形式是源代码，软件系统的可靠性需要源代码的可靠来保证。伴随这软件规模的增长，软件开发的周期越来越长，如何保证源代码的正确性一直是计算机学界研究的重点和热点问题。模型检测技术是一种常见的形式化方法，该方法最初用于硬件设计验证和协议分析。伴随着各种软件问题的出现，研究者提出用模型检测技术验证软件中的相关特征或性质是否满足系统需求或设计要求，这一技术近年来已经被用于针对软件源程序级的验证。
　　本文提出了一种基于模型检测技术的源代码级的验证方法。本方法通过对源代码的抽象语法信息的分析以及与SPIN模型检测工具输入语言Promela的比较，给出了一种从C语言源代码到Promela语言的转换方法。通过这种转换，我们可以得到与C源代码一致的Promela模型，从而可以借助SPIN模型检测工具来间接地验证C语言源代码中的相关性质。
　　本文所做的主要工作包括如下几个部分:
　　首先，通过对源代码的抽象语法信息的分析，得到与源代码对应的控制流图结构，该控制流图结构作为下一步转换工作的基础;
　　其次，对Promela语言和C语言抽象语法信息进行了比较分析，给出了包括控制结构、函数和指针在内的相应转换规则;
　　最后，在上述转换规则的基础上，实现了一个原型工具，能够完成从CFG到Promela的转换，并且实现用SPIN进行指定性质的验证。

目录

声明

摘要

第一章 绪论

1．1 研究动因

1．2 当前的研究现状

1．2．1 国外的研究现状

1．2．2 国内的研究现状

1．2．3 存在的问题

1．3 本文的研究目标与工作

1．4 论文的组织结构

第二章 研究基础

2．1 模型检测方法

2．1．1 模型检测的过程

2．1．2 Buchi自动机

2．1．3 时态逻辑

2．1．4 应对状态空间爆炸的策略

2．2 SPIN模型检测工具

2．2．1 SPIN的结构

2．2．2 SPIN的原理

2．3 Promela的语法

2．3．1 关键字与数据结构

2．3．2 表达式和语句

2．3．3 控制流

2．3．4 进程

2．4 Promela与C语言的比较

2．5 本章小结

第三章 基于模型检测技术的源代码验证方法

3．1 基于模型检测技术的源代码验证原理

3．2 从源代码到CFG的转换方法

3．2．1 C源代码到自定义结构AST的转换

3．2．2 通过AST生成CFG

3．3 从CFG到Promela语言的转换方法

3．3．1 数据类型的转换规则

3．3．2 运算符和语句的转换规则

3．3．3 控制结构的转换规则

3．3．4 指针相关的转换规则

3．3．5 函数的转换方法

3．3．6 CFG到Promela转换的算法

3．4 本章小结

第四章 实验结果及分析

4．1 实验所用示例程序

4．2 生成示例程序的CFG

4．3 根据CFG生成Promela表示

4．4 基于SPIN的性质验证

4．5 本章小结

第五章 总结和展望

5．1 本文工作的总结

5．2 进一步的研究工作

参考文献

在校期间参加的科研项目和发表的论文

致谢