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

【相似文獻(xiàn)】

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1 ;做個RPG游戲主人翁[N];電腦報;2004年

2 廣東 智軒;《做個RPG游戲主人翁》重點回顧[N];電腦報;2004年

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

本文編號：2765744