軟件定義網(wǎng)絡(luò)（Software-Defined Networking,SDN）是一種新興的網(wǎng)絡(luò)架構(gòu),能夠解決傳統(tǒng)網(wǎng)絡(luò)層級復(fù)雜,以至難以管理和創(chuàng)新的問題。該架構(gòu)將控制邏輯從轉(zhuǎn)發(fā)設(shè)備上分離出來,形成邏輯上集中的中心控制器,并提供網(wǎng)絡(luò)可編程性。SDN的出現(xiàn)不僅推動了網(wǎng)絡(luò)架構(gòu)的更迭,更帶來了網(wǎng)絡(luò)開發(fā)方法的變革,可以預(yù)見在未來的網(wǎng)絡(luò)開發(fā)流程之中,形式化方法必定處于極其重要的地位。本文通過形式化方法建模SDN并驗(yàn)證相關(guān)性質(zhì)。對于與數(shù)據(jù)轉(zhuǎn)發(fā)邏輯有關(guān)的性質(zhì),擴(kuò)展了知名的軟件定義網(wǎng)絡(luò)編程語言NetKAT,提出了能描述虛擬局域網(wǎng)（VLAN）、擁有更強(qiáng)表達(dá)能力并且支持模型檢測的語言PDNet,研究了PDNet的操作語義,并基于操作語義證明了PDNet和NetKAT在表達(dá)能力上的聯(lián)系與差別。對于與SDN模塊或應(yīng)用的設(shè)計(jì)、功能和安全有關(guān)的性質(zhì),基于圖靈獎得主C.A.R.Hoare教授提出的通信順序進(jìn)程（CSP）設(shè)計(jì)了系統(tǒng)建�？蚣�,并在模型檢測工具PAT（Process Analysis Toolkit）中進(jìn)行了實(shí)現(xiàn)�；谠摽蚣�,本文建模并驗(yàn)證了開源控制器Floodlight的基礎(chǔ)模塊以及安全控制器TopoGua... 

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

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

【文章目錄】：
摘要
Abstract
第一章 緒論
    1.1 研究背景和動機(jī)
    1.2 研究現(xiàn)狀和相關(guān)工作
    1.3 本文的主要工作
    1.4 本文的組織結(jié)構(gòu)
第二章 背景知識
    2.1 軟件定義網(wǎng)絡(luò)
    2.2 虛擬局域網(wǎng)
    2.3 形式語言與形式語義
    2.4 NetKAT語言
    2.5 本章小結(jié)
第三章 網(wǎng)絡(luò)編程語言PDNet
    3.1 NetKAT的第二種操作語義
    3.2 PDNet語言
    3.3 NetKAT與PDNet對比與證明
    3.4 本章小結(jié)
第四章 SDN系統(tǒng)建�？蚣�
    4.1 框架概述
    4.2 轉(zhuǎn)發(fā)設(shè)備模型
    4.3 主機(jī)模型
    4.4 攻擊者模型
    4.5 本章小節(jié)
第五章 Floodlight控制器的建模與驗(yàn)證
    5.1 Floodlight基本模塊
    5.2 Floodlight模型
    5.3 系統(tǒng)模型與驗(yàn)證
    5.4 本章小節(jié)
第六章 TopoGuard安全機(jī)制的建模與驗(yàn)證
    6.1 Topo Guard機(jī)制
    6.2 Topo Guard模型
    6.3 系統(tǒng)模型與驗(yàn)證
    6.4 改進(jìn)的Topo Guard建模與驗(yàn)證
    6.5 本章小節(jié)
第七章 總結(jié)與展望
    7.1 本文工作總結(jié)
    7.2 后續(xù)工作展望
參考文獻(xiàn)
致謝
研究成果


【參考文獻(xiàn)】：
期刊論文
[1]軟件定義網(wǎng)絡(luò)（SDN）研究進(jìn)展[J]. 張朝昆,崔勇,唐翯翯,吳建平.  軟件學(xué)報(bào). 2015(01)
[2]基于OpenFlow的SDN技術(shù)研究[J]. 左青云,陳鳴,趙廣松,邢長友,張國敏,蔣培成.  軟件學(xué)報(bào). 2013(05)

博士論文
[1]基于質(zhì)量演算的無線網(wǎng)絡(luò)形式語義與分析[D]. 吳茜.華東師范大學(xué) 2016



本文編號：3702130