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

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

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

【學位級別】：博士

【部分圖文】：

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

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

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


本文編號：2901622