本文選題：形式化方法 + L-π演算�。� 參考：《哈爾濱工程大學》2014年碩士論文

【摘要】：集成了計算機技術、通信技術、半導體技術的無線傳感器網(wǎng)絡能夠根據(jù)用戶的需求對各種監(jiān)測對象進行實時的信息采集、處理,具有非常廣泛的應用前景,對擴寬人類的認知領域、改變人類認知方式有巨大的推動作用。與傳統(tǒng)的網(wǎng)絡相比,無線傳感器網(wǎng)絡有一些獨有的特點,網(wǎng)絡的節(jié)點數(shù)量大、面向任務、大規(guī)模自組網(wǎng)、安全性較差、以數(shù)據(jù)為中心,能量受限等,上述這些問題使無線傳感器網(wǎng)絡的設計面臨著諸多問題。其中,通信協(xié)議的設計是無線傳感器網(wǎng)絡中的關鍵問題之一。形式化方法在無線傳感器網(wǎng)絡路由協(xié)議的設計中不但可以提高協(xié)議的開發(fā)效率,而且有助于精確地完成性能的分析和性質的驗證,改善網(wǎng)絡協(xié)議的設計質量。本文根據(jù)無線傳感器節(jié)點通信范圍受限的特性,對π演算進行擴展,提出一種能夠描述與驗證無線傳感器網(wǎng)絡路由協(xié)議的形式化方法,L-π演算。為了能夠在節(jié)點層次上描述無線傳感器網(wǎng)絡的通信行為,本文定義了 L-π演算的表達式,在基本π演算的語法中加入了鄰居節(jié)點列表;定義了 L-π演算的動作集合,加入了廣播動作描述節(jié)點的廣播通信行為。其次,為了定義不同節(jié)點表達式間的等價關系,在節(jié)點層次上定義了結構同余規(guī)則,定義了節(jié)點間結構同余的轄域律,交換律,浮動律;為了規(guī)定節(jié)點間的交互行為,定義了節(jié)點間的轉換規(guī)則。重新論證了節(jié)點間的強模擬、基于結構同余的強模擬以及弱模擬理論,利用互模擬理論分析與驗證了無線傳感器網(wǎng)絡的性質。最后,利用L-π演算描述了無線傳感器網(wǎng)絡路由協(xié)議中的信息傳感協(xié)議和簇頭選擇協(xié)議,通過實驗驗證了利用L-π描述的上述協(xié)議的正確性,分析了實驗的優(yōu)點與不足。
[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

【參考文獻】

相關期刊論文 前4條

1 沈波;張世永;鐘亦平;;無線傳感器網(wǎng)絡分簇路由協(xié)議[J];軟件學報;2006年07期

2 崔莉,鞠海玲,苗勇,李天璞,劉巍,趙澤;無線傳感器網(wǎng)絡研究進展[J];計算機研究與發(fā)展;2005年01期

3 于海斌,曾鵬,王忠鋒,梁英,尚志軍;分布式無線傳感器網(wǎng)絡通信協(xié)議研究[J];通信學報;2004年10期

4 董紅斌,楊巨慶;Petri網(wǎng):概念、分析方法和應用[J];哈爾濱師范大學自然科學學報;1999年05期

相關博士學位論文 前3條

1 袁久銀;無線傳感器網(wǎng)絡節(jié)點能量均衡策略及控制算法研究[D];重慶大學;2009年

2 周集良;無線傳感器網(wǎng)絡路由協(xié)議的安全與優(yōu)化研究[D];東華大學;2009年

3 王媛麗;無線傳感器網(wǎng)絡中路由相關的若干問題的研究[D];國防科學技術大學;2006年

相關碩士學位論文 前7條

1 王冰;基于能量均衡的無線傳感器網(wǎng)絡覆蓋算法[D];吉林大學;2013年

2 馬嵐;水下機器人協(xié)同仿真模型組合方法的研究[D];哈爾濱工程大學;2012年

3 高鶯;礦山井下無線傳感器網(wǎng)絡多徑路由協(xié)議的研究[D];北京交通大學;2010年

4 仲新林;無線傳感器網(wǎng)絡中地理位置路由協(xié)議研究[D];南京航空航天大學;2010年

5 宋艷;基于能量均衡的無線傳感器網(wǎng)絡路由協(xié)議[D];西安電子科技大學;2010年

6 姚仲歡;無線傳感器網(wǎng)絡中基于網(wǎng)絡拓撲與路由的節(jié)能技術研究[D];廣西大學;2008年

7 年曉玲;基于擴展有限狀態(tài)機軟件測試用例自動生成的研究[D];西南交通大學;2005年

，

本文編號：2074480