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

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

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

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

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

【部分圖文】：

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

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

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


本文編號：2901622