基于π演算的WSN路由协议形式化验证的方法研究

摘要

集成了计算机技术、通信技术、半导体技术的无线传感器网络能够根据用户的需求对各种监测对象进行实时的信息采集、处理，具有非常广泛的应用前景，对扩宽人类的认知领域、改变人类认知方式有巨大的推动作用。与传统的网络相比，无线传感器网络有一些独有的特点，网络的节点数量大、面向任务、大规模自组网、安全性较差、以数据为中心，能量受限等，上述这些问题使无线传感器网络的设计面临着诸多问题。其中，通信协议的设计是无线传感器网络中的关键问题之一。形式化方法在无线传感器网络路由协议的设计中不但可以提高协议的开发效率，而且有助于精确地完成性能的分析和性质的验证，改善网络协议的设计质量。
　　本文根据无线传感器节点通信范围受限的特性，对π演算进行扩展，提出一种能够描述与验证无线传感器网络路由协议的形式化方法，L-π演算。为了能够在节点层次上描述无线传感器网络的通信行为，本文定义了L-π演算的表达式，在基本π演算的语法中加入了邻居节点列表；定义了L-π演算的动作集合，加入了广播动作描述节点的广播通信行为。其次，为了定义不同节点表达式间的等价关系，在节点层次上定义了结构同余规则，定义了节点间结构同余的辖域律，交换律，浮动律；为了规定节点间的交互行为，定义了节点间的转换规则。重新论证了节点间的强模拟、基于结构同余的强模拟以及弱模拟理论，利用互模拟理论分析与验证了无线传感器网络的性质。最后，利用L-π演算描述了无线传感器网络路由协议中的信息传感协议和簇头选择协议，通过实验验证了利用L-π描述的上述协议的正确性，分析了实验的优点与不足。

目录

封面

声明

中文摘要

英文摘要

目录

第1章 绪论

1.1 研究背景及意义

1.2相关领域现状

1.3主要研究内容

第2章 相关理论与技术

2.1无线传感器网络体系结构

2.2无线传感器网络路由协议的分析

2.3 形式化方法概述

2.4本章小结

第3章 L-π演算

3.1π演算简介

3.2 L-π演算的定义

3.3 L-π演算的互模拟理论

3.4 WSN行为的形式化描述与分析

3.5本章小结

第4章 基于L-π演算的WSN路由协议形式化验证

4.1WSN路由协议的形式化描述

4.2 L-π演算有效性的验证及分析

4.3本章小结

结论

参考文献

致谢