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

发布时间：2018-06-27 16:11

本文选题：形式化方法 + L-π演算　；参考：《哈尔滨工程大学》2014年硕士论文

【摘要】：集成了计算机技术、通信技术、半导体技术的无线传感器网络能够根据用户的需求对各种监测对象进行实时的信息采集、处理,具有非常广泛的应用前景,对扩宽人类的认知领域、改变人类认知方式有巨大的推动作用。与传统的网络相比,无线传感器网络有一些独有的特点,网络的节点数量大、面向任务、大规模自组网、安全性较差、以数据为中心,能量受限等,上述这些问题使无线传感器网络的设计面临着诸多问题。其中,通信协议的设计是无线传感器网络中的关键问题之一。形式化方法在无线传感器网络路由协议的设计中不但可以提高协议的开发效率,而且有助于精确地完成性能的分析和性质的验证,改善网络协议的设计质量。本文根据无线传感器节点通信范围受限的特性,对π演算进行扩展,提出一种能够描述与验证无线传感器网络路由协议的形式化方法,L-π演算。为了能够在节点层次上描述无线传感器网络的通信行为,本文定义了 L-π演算的表达式,在基本π演算的语法中加入了邻居节点列表;定义了 L-π演算的动作集合,加入了广播动作描述节点的广播通信行为。其次,为了定义不同节点表达式间的等价关系,在节点层次上定义了结构同余规则,定义了节点间结构同余的辖域律,交换律,浮动律;为了规定节点间的交互行为,定义了节点间的转换规则。重新论证了节点间的强模拟、基于结构同余的强模拟以及弱模拟理论,利用互模拟理论分析与验证了无线传感器网络的性质。最后,利用L-π演算描述了无线传感器网络路由协议中的信息传感协议和簇头选择协议,通过实验验证了利用L-π描述的上述协议的正确性,分析了实验的优点与不足。
[Abstract]:The wireless sensor network, which integrates computer technology, communication technology and semiconductor technology, can collect and process real-time information for various monitoring objects according to the needs of users. It has a very wide application prospect. It can greatly promote the expansion of human cognitive field and the change of human cognitive style. Compared with traditional networks, wireless sensor networks have some unique characteristics, such as large number of nodes, mission oriented, large-scale ad hoc networks, poor security, data-centric, energy constraints, etc. These problems make the design of wireless sensor network face many problems. The design of communication protocol is one of the key problems in wireless sensor networks. The formal method can not only improve the efficiency of protocol development, but also improve the performance analysis and property verification, and improve the design quality of wireless sensor network routing protocol. According to the limited communication range of wireless sensor nodes, this paper extends 蟺 calculus, and proposes a formal method for describing and verifying routing protocols in wireless sensor networks, called L- 蟺 calculus. In order to describe the communication behavior of wireless sensor networks at node level, the expression of L- 蟺 calculus is defined, the list of neighbor nodes is added to the syntax of basic 蟺 calculus, and the action set of L- 蟺 calculus is defined. The broadcast action is added to describe the broadcast communication behavior of the node. Secondly, in order to define the equivalence relation between different node expressions, the structural congruence rules are defined at the node level, the domain law, exchange law and floating law of structural congruence among nodes are defined, and the interaction behavior between nodes is defined. The transformation rules between nodes are defined. Based on the theory of strong simulation and weak simulation of structural congruence, the properties of wireless sensor networks are analyzed and verified by using the theory of mutual simulation. Finally, the information sensing protocol and cluster head selection protocol in wireless sensor network routing protocol are described by L- 蟺 calculus. The correctness of the protocol described by L- 蟺 is verified by experiments, and the advantages and disadvantages of the experiment are analyzed.
【学位授予单位】：哈尔滨工程大学
【学位级别】：硕士
【学位授予年份】：2014
【分类号】：TP212.9;TN929.5

【参考文献】