基于关系数据理论的函数型程序似然不变量动态检测方法

论文摘要

随着计算机技术的发展,软件在各个行业得到广泛的应用,人们对软件的质量和安全也得到更为广泛的关注。对如何提高软件质量的问题人们已经从软件开发方法、软件开发过程管理、软件开发工具等多个方面加以研究,取得了一定的成绩。基于合约的软件开发是其中十分重要且得到广泛应用的一种技术。软件合约是指软件中必须遵守的规则。开发者和执行者通过遵守这些合约来保证软件的质量。从不同的层面合约可分为语法合约、数据合约、行为合约和服务合约。程序不变量是数据合约的一种形式。程序不变量对于程序演进与重构、程序测试与排错、辅助定理证明、构件升级替换都有重要作用。由于大多数软件开发时都没有书写形式化文档,程序不变量在程序中很少被清楚地表示出来。如何从程序中发现这些隐含的没有被程序员写出来的程序不变量成为实现高层次行为合约、提高程序质量的关键。本文重点研究如何使用动态检测技术发现程序中函数型似然不变量。论文首先介绍了不变量动态检测技术及其主要的两个实现工具:Daikon和DIDUCE,并分析了它们在编配工具和不变量检测方法上存在的不足。然后运用面向对象的软件开发方法,设计并实现了一个新的基于关系数据库的编配工具。新的编配工具具有易用、灵活等特点。结合关系数据理论,针对函数型不变量提出了一个启发式不变量检测方法。该方法通过函数推导技术首先确定待检变量中是否存在函数依赖关系,然后再进行函数解析式推导,解决了传统似然不变量检测方法中存在的盲目性问题。并对新方法和传统方法进行了对比实验分析,实验结果表明新方法的可靠性与检测效率明显优于传统方法。

论文目录

• 摘要
• ABSTRACT
• 第一章 绪论
• 1.1 研究背景
• 1.2 研究现状
• 1.3 本文的组织结构
• 第二章 程序似然不变量的动态检测技术
• 2.1 程序分析技术
• 2.2 程序似然不变量检测技术
• 2.3 Daikon
• 2.4 DIDUCE
• 2.5 小结
• 第三章 基于关系数据库的程序似然不变量编配工具
• 3.1 程序编配工具分析
• 3.2 编配工具设计
• 3.2.1 用例图
• 3.2.2 结构图
• 3.2.3 类图
• 3.2.4 时序图
• 3.3 检测工具实现
• 3.4 小结
• 第四章 基于关系数据理论的检测方法
• 4.1 不变量检测试探法
• 4.2 函数型不变量
• 4.3 关系数据理论
• 4.3.1 关系数据模型
• 4.3.2 函数依赖推导
• 4.4 基于关系数据理论的检测方法
• 4.5 实验分析
• 4.5.1 实验设计
• 4.5.2 实验分析
• 4.6 小结
• 第五章 总结展望
• 5.1 工作总结
• 5.2 工作展望
• 参考文献
• 成果目录
• 致谢