隨著軟件定義網(wǎng)絡(luò)（software-defined network,簡(jiǎn)稱(chēng)SDN）規(guī)模的擴(kuò)大和上層應(yīng)用的復(fù)雜化,單個(gè)控制器已經(jīng)不能滿足網(wǎng)絡(luò)要求,成為網(wǎng)絡(luò)性能的瓶頸。多控制器集群管理SDN有很多優(yōu)勢(shì),但實(shí)現(xiàn)多控制器架構(gòu)需要解決的最基本問(wèn)題是多控制器之間保持一致性。在集群中運(yùn)行Raft一致性算法可以解決一致性問(wèn)題,但集群中Leader被重新選舉時(shí)會(huì)導(dǎo)致集群不可用。因此本文從集群的可用性出發(fā),為Raft算法增加領(lǐng)導(dǎo)權(quán)轉(zhuǎn)移功能,避免因Leader被要求關(guān)閉、移出集群等情形導(dǎo)致的集群不可用。本文主要研究?jī)?nèi)容有:第一,對(duì)Raft算法選舉部分可以轉(zhuǎn)移領(lǐng)導(dǎo)權(quán)的情形進(jìn)行詳細(xì)分類(lèi),給出選擇目標(biāo)節(jié)點(diǎn)的度量與方法。針對(duì)多控制器集群的工作特點(diǎn),選取合適的指標(biāo)選擇目標(biāo)控制器。第二,使用TLA+語(yǔ)言對(duì)領(lǐng)導(dǎo)權(quán)轉(zhuǎn)移功能進(jìn)行形式化描述,并使用TLC工具對(duì)增加領(lǐng)導(dǎo)權(quán)轉(zhuǎn)移的Raft算法的形式化描述進(jìn)行檢測(cè)與驗(yàn)證,從而證明其正確性。第三,討論多控制器集群中Raft算法的運(yùn)行環(huán)境,使用TLA+語(yǔ)言描述并使用TLC工具對(duì)規(guī)約進(jìn)行檢測(cè)與驗(yàn)證。第四,分析了OpenDaylight（ODL）代碼中的Raft算法源碼的領(lǐng)導(dǎo)權(quán)轉(zhuǎn)移部分,并對(duì)選... 

【文章來(lái)源】：內(nèi)蒙古大學(xué)內(nèi)蒙古自治區(qū) 211工程院校

【文章頁(yè)數(shù)】：69 頁(yè)

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

【部分圖文】：

選舉算法規(guī)約檢測(cè)模型

圖 4.2 選舉算法規(guī)約檢測(cè)結(jié)果Figure 4.2 The checking results for election algorithm specification4.4 Raft 算法中 Leader 領(lǐng)導(dǎo)權(quán)轉(zhuǎn)移的行為描述.4.1 狀態(tài)轉(zhuǎn)換行為和消息處理行為由 3.3.3 節(jié)可知，由于 Raft 算法的選舉部分有選舉限制條件，因此 Raft 算法中領(lǐng)導(dǎo)權(quán)的具體步驟與將選舉算法中領(lǐng)導(dǎo)權(quán)轉(zhuǎn)移的具體步驟不同，導(dǎo)致形式化描述也不相同。將權(quán)轉(zhuǎn)移的形式化描述加入 Raft 算法時(shí)與加入選舉算法時(shí)有下述幾點(diǎn)不同。第一是發(fā)生領(lǐng)轉(zhuǎn)移時(shí)集群需要停止接收交換機(jī)的請(qǐng)求，除了加入 Receiverequest(i, v)行為外，Raft 算法化描述中原有的行為 ClientRequest(i, v)行為將增加一個(gè)發(fā)生的條件，表示可以放入 Lea志中的請(qǐng)求屬于控制器中存儲(chǔ)的交換機(jī)請(qǐng)求隊(duì)列，即加入語(yǔ)句 v∈RequestQueue。第二點(diǎn)

SDN 多控制器環(huán)境下對(duì) Raft 一致性算法的改進(jìn)及正確性證明4.5 Raft 算法的 TLC 檢測(cè)和驗(yàn)證增加領(lǐng)導(dǎo)權(quán)轉(zhuǎn)移的 Raft 算法進(jìn)行形式化描述后，使用模型檢測(cè)工具 TLC 對(duì)上述。首先創(chuàng)建一個(gè) Model，命名為 Model_1，然后給常量賦值。常量 Server 代表合，賦值為集合{1,2,3,4,5}；常量 LoadMin 與 LoadMax 賦值常數(shù) 10 和 20；常集合{1..10}；其他常量均賦值為 TLC 工具自帶的 Model Value。檢測(cè)初始狀態(tài)步關(guān)系 Next，并檢測(cè)規(guī)約是否會(huì)死鎖，如圖 4.3 所示。模型檢測(cè)結(jié)果如圖 4.4 所表明，模型檢測(cè)器一直運(yùn)行，檢測(cè)執(zhí)行及關(guān)閉時(shí)沒(méi)有拋出異常，說(shuō)明規(guī)約沒(méi)有

【參考文獻(xiàn)】：
期刊論文
[1]一種軟件定義網(wǎng)絡(luò)中的控制器熱備份及選舉算法[J]. 王文博,汪斌強(qiáng),陳飛宇,王志明,宮陽(yáng)陽(yáng).  電子學(xué)報(bào). 2016(04)
[2]基于行為時(shí)序邏輯TLA的Pastry協(xié)議的規(guī)約與驗(yàn)證[J]. 劉照洋,龍士工.  貴州大學(xué)學(xué)報(bào)(自然科學(xué)版). 2015(06)
[3]SDN和NFV對(duì)網(wǎng)絡(luò)變革發(fā)展影響綜述[J]. 張志強(qiáng).  現(xiàn)代電信科技. 2015(01)
[4]SDN控制器的調(diào)研和量化分析[J]. 江國(guó)龍,付斌章,陳明宇,張立新.  計(jì)算機(jī)科學(xué)與探索. 2014(06)
[5]基于TLA+的AFDX冗余管理算法的改進(jìn)[J]. 庫(kù)恒,龍士工,羅昊.  計(jì)算機(jī)工程與設(shè)計(jì). 2013(03)
[6]基于TLA的ARQ協(xié)議描述與驗(yàn)證[J]. 吳勇,李祥.  計(jì)算機(jī)安全. 2012(08)
[7]分布式超級(jí)節(jié)點(diǎn)選舉算法[J]. 杜麗娟,余鎮(zhèn)危.  計(jì)算機(jī)工程與應(yīng)用. 2011(14)
[8]ARP協(xié)議的描述與TLA驗(yàn)證[J]. 李元,吳勇,李祥.  計(jì)算機(jī)技術(shù)與發(fā)展. 2010(06)
[9]基于TLA+的BRP協(xié)議規(guī)約及驗(yàn)證[J]. 陳立前,王戟,陳火旺.  計(jì)算機(jī)工程與科學(xué). 2006(01)

碩士論文
[1]PAXOS算法改進(jìn)及應(yīng)用研究[D]. 劉春漲.廣西民族大學(xué) 2016
[2]基于Zookeeper的SDN多控制器架構(gòu)的研究與實(shí)現(xiàn)[D]. 田心寧.蘭州大學(xué) 2016
[3]基于行為時(shí)序邏輯TLA的網(wǎng)絡(luò)協(xié)議的描述與驗(yàn)證[D]. 劉照洋.貴州大學(xué) 2015



本文編號(hào)：2936149