基于有界模型检验的传感网软件验证方法研究

摘要

传感网是一种由具有感知、处理和无线通信能力的传感器节点通过自组织方式形成的一种多跳网络。随着传感网的迅速发展，传感网软件的规模逐渐变大，这使得不同的应用领域对传感网软件的性能都有着越来越高的要求。软件验证技术是保证软件性能的一项重要技术。模型检验是软件验证技术的一种，它为传感网软件验证提供了新的技术手段。在基于模型检验的软件验证领域中，状态空间爆炸问题是其发展的瓶颈。有界模型检验技术是模型检验领域新的研究方向，它通过限制建立模型时状态展开的次数来实现，主要用于缓解状态空间爆炸问题。
　　本文主要对基于有界模型检验的传感网软件验证方法进行研究，该研究是面向源代码的，其实现主要分为两个工作：
　　1）提出一种基于有界模型检验的传感网软件代码验证方法。该方法首先通过对传感网软件建立软件模型，实现对传感网软件的静态结构和动态行为的抽象；然后定义模型转换规则，将软件模型转化C语言代码；最后使用CBMC对转化后的代码进行有界模型检验。
　　2）提出一种基于POR（偏序简约）的有界模型检验优化算法，该算法通过分段的方法来避免重复路径的搜索，较少状态遍历时间。

目录

封面

声明

中文摘要

英文摘要

目录

第一章 绪论

1.1课题研究背景和意义

1.2国内外研究现状

1.3论文内容以及结构安排

第二章 相关工作

2.1传感网基本概念

2.2传感网软件验证

2.3模型检验技术

2.4本章小结

第三章 基于有界模型检验的传感网软件代码验证方法

3.1引言

3.2基于模型检验的传感网软件代码分析

3.3基于有界模型检验的转换规则

3.4传感网软件代码验证分析

3.5本章小结

第四章 基于模型检验的传感网软件验证优化

4.1引言

4.2基于改进的POR的验证优化算法

4.3基于改进的POR的验证优化算法

4.4验证分析

4.5本章小结

第五章 总结与展望

5.1工作总结

5.2进一步研究展望

参考文献

附录1攻读硕士学位期间申请的专利

附录2攻读硕士学位期间参加的科研项目

致谢