【摘要】：基于形式化方法的協(xié)議一致性測(cè)試是確保協(xié)議可靠性的基本手段。當(dāng)前,一些新型互聯(lián)網(wǎng)協(xié)議中存在不同的并行組件,而傳統(tǒng)形式化方法難以描述這些特點(diǎn),本文針對(duì)基于擴(kuò)展并行多組件狀態(tài)機(jī)的網(wǎng)絡(luò)協(xié)議測(cè)試進(jìn)行了深入的研究。本文綜述了相關(guān)的研究現(xiàn)狀,指出單一組件模型難以描述多組件的協(xié)議,而現(xiàn)有的多組件模型也難以描述組件間共享數(shù)據(jù)的情況;軟件定義網(wǎng)絡(luò)是帶有并行多組件的新型互聯(lián)網(wǎng)協(xié)議的典型代表,但尚缺少采用形式化方法的黑盒測(cè)試。本文研究了擴(kuò)展并行多組件狀態(tài)機(jī)的建�？蚣�,分別提出了三種不同的擴(kuò)展并行多組件狀態(tài)機(jī)模型:為了描述并行組件間采用共享數(shù)據(jù)通信的情況,提出了讀取外部變量的并行擴(kuò)展有限狀態(tài)機(jī)模型;為了描述多級(jí)流水線結(jié)構(gòu),提出了流水線擴(kuò)展有限狀態(tài)機(jī)模型,其同級(jí)組件間存在共享變量讀寫,跨級(jí)組件間存在單向消息傳遞;將消息傳遞與網(wǎng)絡(luò)拓?fù)浣Y(jié)合,提出了信息表擴(kuò)展有限狀態(tài)機(jī)模型。本文提出了基于定義使用路徑的并行擴(kuò)展有限狀態(tài)機(jī)測(cè)試生成方法。首先生成內(nèi)部變量的定義使用路徑,然后使其可執(zhí)行化并生成外部變量的定義使用路徑。該方法是啟發(fā)式方法,可用于變量無限取值的模型并避免狀態(tài)空間爆炸。本文提出了基于可達(dá)圖的并行擴(kuò)展有限狀態(tài)機(jī)層次化測(cè)試生成方法。該方法適用于變量取值有限的模型,其使用自底向上的可達(dá)圖生成緩解狀態(tài)空間爆炸,同時(shí)使用自頂向下的測(cè)試序列生成確保可執(zhí)行。將前述兩種測(cè)試生成方法分別應(yīng)用于源地址驗(yàn)證協(xié)議測(cè)試,驗(yàn)證了方法的有效性。本文提出了流水線擴(kuò)展有限狀態(tài)機(jī)測(cè)試生成方法。首先將模型轉(zhuǎn)換為數(shù)據(jù)圖并找到數(shù)據(jù)路徑;然后生成數(shù)據(jù)路徑上的組件狀態(tài)機(jī)的前導(dǎo)序列并組成測(cè)試序列。通過實(shí)驗(yàn)對(duì)比表明該方法能夠生成系統(tǒng)覆蓋模型的測(cè)試集,并有效控制了測(cè)試生成的時(shí)間和空間開銷。將本方法應(yīng)用于Open Flow交換機(jī)的一致性測(cè)試,發(fā)現(xiàn)了協(xié)議實(shí)現(xiàn)中的錯(cuò)誤和協(xié)議中值得討論的問題。本文提出了信息表擴(kuò)展有限狀態(tài)機(jī)測(cè)試生成方法。對(duì)于設(shè)計(jì)缺陷,用模型檢測(cè)工具根據(jù)模型生成反例;對(duì)于實(shí)現(xiàn)錯(cuò)誤,綜合運(yùn)用組件部分組合、拓?fù)鋵?duì)稱化簡(jiǎn)和拓?fù)淠M執(zhí)行生成擴(kuò)展測(cè)試序列。該方法能夠同時(shí)檢測(cè)設(shè)計(jì)缺陷和實(shí)現(xiàn)錯(cuò)誤,而且在與網(wǎng)絡(luò)拓?fù)浣Y(jié)合的同時(shí),減緩狀態(tài)空間爆炸的風(fēng)險(xiǎn)。
【學(xué)位授予單位】：清華大學(xué)
【學(xué)位級(jí)別】：博士
【學(xué)位授予年份】：2015
【分類號(hào)】：TP393.04

【相似文獻(xiàn)】

相關(guān)期刊論文 前10條

1 黃勇;;游戲中的狀態(tài)機(jī)[J];程序員;2008年12期

2 丘映瑩;;復(fù)雜層次狀態(tài)機(jī)的一種解決方案[J];煤炭技術(shù);2013年03期

3 張俊;;狀態(tài)機(jī)思路在單片機(jī)程序設(shè)計(jì)中的應(yīng)用[J];今日電子;2009年02期

4 聶旭中;;狀態(tài)機(jī)設(shè)計(jì)研究[J];洛陽師范學(xué)院學(xué)報(bào);2009年02期

5 徐東明,黃海生;電路設(shè)計(jì)狀態(tài)機(jī)描述算法研究[J];微電子學(xué)與計(jì)算機(jī);2001年02期

6 羅宏洋;;狀態(tài)機(jī)在離子注入機(jī)中的應(yīng)用[J];電子工業(yè)專用設(shè)備;2009年09期

7 劉暉,李明祿;基于抽象狀態(tài)機(jī)的網(wǎng)格系統(tǒng)設(shè)計(jì)和分析[J];電子學(xué)報(bào);2003年S1期

8 楊朝紅;劉海燕;肖慶;;基于擴(kuò)展?fàn)顟B(tài)機(jī)的資源泄漏檢測(cè)方法[J];裝甲兵工程學(xué)院學(xué)報(bào);2009年01期

9 馮學(xué)偉;王東霞;馬國(guó)慶;李津;;基于狀態(tài)機(jī)的入侵場(chǎng)景重構(gòu)關(guān)鍵技術(shù)研究[J];微型機(jī)與應(yīng)用;2010年17期

10 王詠武;;瘋狂的火星蟲——面向?qū)ο鬆顟B(tài)機(jī)實(shí)踐指南[J];程序員;2004年08期

相關(guān)會(huì)議論文 前3條

1 易劍;馬亞平;朱冰;;基于BOM的組合模型描述方法研究[A];2013第一屆中國(guó)指揮控制大會(huì)論文集[C];2013年

2 周建;王健;;μC/OS的層次式狀態(tài)機(jī)在人機(jī)界面中的應(yīng)用[A];浙江省電子學(xué)會(huì)2010學(xué)術(shù)年會(huì)論文集[C];2010年

3 楊盛光;周干民;林大雋;高明倫;;基于狀態(tài)機(jī)的IIC總線接口封裝[A];全國(guó)第十五屆計(jì)算機(jī)科學(xué)與技術(shù)應(yīng)用學(xué)術(shù)會(huì)議論文集[C];2003年

相關(guān)重要報(bào)紙文章 前3條

1 ;做個(gè)RPG游戲主人翁[N];電腦報(bào);2004年

2 廣東 智軒;《做個(gè)RPG游戲主人翁》重點(diǎn)回顧[N];電腦報(bào);2004年

3 北京大學(xué)信息科學(xué)與技術(shù)學(xué)院　馬浩�！∩劬S忠　麻志毅;UML 2.0修成正果[N];計(jì)算機(jī)世界;2003年

相關(guān)博士學(xué)位論文 前2條

1 姚姜源;基于擴(kuò)展并行多組件狀態(tài)機(jī)的網(wǎng)絡(luò)協(xié)議測(cè)試研究[D];清華大學(xué);2015年

2 阮堅(jiān);異步控制電路設(shè)計(jì)與實(shí)現(xiàn)關(guān)鍵技術(shù)研究[D];國(guó)防科學(xué)技術(shù)大學(xué);2008年

相關(guān)碩士學(xué)位論文 前10條

1 賀增川;基于狀態(tài)機(jī)的微模塊化程序設(shè)計(jì)技術(shù)在聲學(xué)滑翔機(jī)中的應(yīng)用研究[D];中國(guó)海洋大學(xué);2015年

2 袁軍;一種基于狀態(tài)機(jī)的數(shù)字邏輯系統(tǒng)的功能驗(yàn)證方法[D];西南交通大學(xué);2009年

3 王欣;基于狀態(tài)機(jī)的移動(dòng)終端應(yīng)用軟件設(shè)計(jì)[D];上海交通大學(xué);2007年

4 林莉;狀態(tài)機(jī)的若干代數(shù)性質(zhì)[D];廣西師范大學(xué);2004年

5 李志軍;基于狀態(tài)機(jī)的安全漏洞檢查機(jī)制的設(shè)計(jì)與實(shí)現(xiàn)[D];西安電子科技大學(xué);2010年

6 陸原;基于狀態(tài)機(jī)的計(jì)費(fèi)系統(tǒng)框架的設(shè)計(jì)[D];復(fù)旦大學(xué);2008年

7 趙海龍;[D];天津大學(xué);2006年

8 尹鵬;基于多值邏輯狀態(tài)機(jī)的需求分歧研究[D];西安理工大學(xué);2007年

9 楊丹丹;基于抽象狀態(tài)機(jī)的協(xié)議軟件測(cè)試方法研究[D];西安電子科技大學(xué);2010年

10 馮凌云;基于狀態(tài)機(jī)AI技術(shù)的網(wǎng)絡(luò)游戲戰(zhàn)斗系統(tǒng)設(shè)計(jì)[D];復(fù)旦大學(xué);2011年

本文編號(hào)：2765744