發(fā)布時(shí)間：2020-12-06 15:39

　　移動(dòng)ad hoc網(wǎng)絡(luò)是由移動(dòng)節(jié)點(diǎn)搭建的臨時(shí)通信網(wǎng)絡(luò)。網(wǎng)絡(luò)中沒有任何固定的基礎(chǔ)設(shè)施和中心管理設(shè)備。因?yàn)楣?jié)點(diǎn)可以自由移動(dòng),網(wǎng)絡(luò)拓?fù)潆S時(shí)可能發(fā)生變化。所以ad hoc路由協(xié)議必須能在動(dòng)態(tài)的環(huán)境中找到從源到目標(biāo)的有效路徑。這使得在此種網(wǎng)絡(luò)中的路由選擇比在有線網(wǎng)絡(luò)中的路由選擇更具有挑戰(zhàn)性。當(dāng)前研究人員已經(jīng)提出許多在可信的網(wǎng)絡(luò)環(huán)境下工作的ad hoc路由協(xié)議,可以分為三類:主動(dòng)式路由協(xié)議、反應(yīng)式路由協(xié)議和混合路由協(xié)議。移動(dòng)ad hoc網(wǎng)絡(luò)中節(jié)點(diǎn)采用無線通信方式,并且沒有固定基礎(chǔ)設(shè)施和中心的安全控制。同固定網(wǎng)絡(luò)相比,移動(dòng)ad hoc網(wǎng)絡(luò)更容易受到物理和通信攻擊。此類網(wǎng)絡(luò)的安全性越來越受到重視�；谠诳尚怒h(huán)境下工作的路由協(xié)議,研究人員提出在非可信環(huán)境下工作的安全ad hoc路由協(xié)議。如何保證研究人員提出的路由協(xié)議或算法的正確性成為一項(xiàng)具有挑戰(zhàn)性的任務(wù)。本文對(duì)當(dāng)前ad hoc路由協(xié)議形式化驗(yàn)證工作進(jìn)行研究,總結(jié)采用Event-B方法從系統(tǒng)需求到形式化建模和驗(yàn)證的分析流程。此外,針對(duì)Event-B不支持時(shí)間屬性描述的問題,提出了任務(wù)級(jí)時(shí)間約束模式。本文的主要貢獻(xiàn)如下:·在可信的網(wǎng)絡(luò)環(huán)境下,大多數(shù)研究者對(duì)單... 

【文章來源】：浙江大學(xué)浙江省 211工程院校 985工程院校 教育部直屬院校

【文章頁數(shù)】：170 頁

【學(xué)位級(jí)別】：博士

【部分圖文】：

圖１．１移動(dòng)ａｄ?ｈｏｃ網(wǎng)絡(luò)??

浙江大學(xué)博士學(xué)位論文?第２章Ｅｖｅｎｔ－Ｂ方法及Ｒｏｄｉｎ工具??ｓｅｅｓ??Ｍａｃｈｉｎｅ?？?Ｃｏｎｔｅｘｔ??ｒｅｆｉｎｅｓ?ｅｘｔｅｎｄｓ??ｓｅｅｓ??Ｍａｃｈｉｎｅ?■?＇■?？?Ｃｏｎｔｅｘｔ??ｅｘｔｅｎｄｓ??ｒｅｆｉｎｅｓ??圖２．１機(jī)器和環(huán)境關(guān)系圖??ｍａｃｈｉｎｅ?Ｍ??

圖２．１機(jī)器和環(huán)境關(guān)系圖??


本文編號(hào)：2901622