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

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

【參考文獻(xiàn)】

相關(guān)期刊論文 前4條

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

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

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

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

相關(guān)博士學(xué)位論文 前3條

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

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

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

相關(guān)碩士學(xué)位論文 前7條

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

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

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

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

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

6 姚仲歡;無線傳感器網(wǎng)絡(luò)中基于網(wǎng)絡(luò)拓?fù)渑c路由的節(jié)能技術(shù)研究[D];廣西大學(xué);2008年

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

，

本文編號(hào)：2074480