本文關(guān)鍵詞：使用模型檢驗自動化驗證路由協(xié)議

  更多相關(guān)文章： 模型檢驗 路由協(xié)議驗證 形式化方法 SPIN CBMC

【摘要】：模型檢驗可驗證路由協(xié)議的收斂性,環(huán)路問題,包交付失敗,由于協(xié)議描述的歧義導(dǎo)致的問題,安全性缺陷等.實驗一建立關(guān)注鏈路狀態(tài)數(shù)據(jù)庫同步的OSPF模型,設(shè)置攻擊者路由器偽造消息,找到攻擊成功的反例;實驗二建立關(guān)注節(jié)點加入、失效和相應(yīng)處理的Chord模型,尋找協(xié)議缺陷.兩個模型都用顯式模型檢驗工具SPIN和有界模型檢驗工具CBMC實現(xiàn)驗證,實驗結(jié)果表明SPIN解決此類問題更有優(yōu)勢.
【作者單位】： 南京航空航天大學(xué)計算機科學(xué)與技術(shù)學(xué)院;
【關(guān)鍵詞】： 模型檢驗 路由協(xié)議驗證 形式化方法 SPIN CBMC
【基金】：國家自然科學(xué)基金項目(61100034)資助 中國博士后科學(xué)基金項目(20110491411,2012T50498)資助 江蘇省博士后科研計劃項目(1101092C)資助
【分類號】：TP393.04
【正文快照】： 1引言模型檢驗是一種基于有限狀態(tài)系統(tǒng)的形式化自動驗證方法,最早由Clarke、Emerson[1]和Queille、Sifakis[2]分別獨立提出.模型檢驗的基本思想是窮盡搜索待驗證模型的有限狀態(tài)空間,檢驗狀態(tài)是否滿足性質(zhì).如果存在狀態(tài)不滿足,生成違反性質(zhì)的反例.隨著模型規(guī)模的增加,并發(fā)系統(tǒng)

【共引文獻(xiàn)】

中國博士學(xué)位論文全文數(shù)據(jù)庫 前1條

1 江健;互聯(lián)網(wǎng)域名系統(tǒng)授權(quán)機制中不一致和多重依賴問題研究[D];清華大學(xué);2013年

【相似文獻(xiàn)】

中國期刊全文數(shù)據(jù)庫 前10條

1 黃蔚;;模型檢驗技術(shù)的研究與應(yīng)用[J];電子質(zhì)量;2008年02期

2 文艷軍;王戟;齊治昌;;并發(fā)反應(yīng)式系統(tǒng)的組合模型檢驗與組合精化檢驗[J];軟件學(xué)報;2007年06期

3 劉恩軍;;基于線性帶權(quán)值的廣義表的模型檢驗方法[J];計算機工程與應(yīng)用;2008年29期

4 董威,王戟,齊治昌;UML Statecharts的切片模型檢驗方法[J];電子學(xué)報;2002年S1期

5 屈婉霞;李暾;郭陽;楊曉東;;模型檢驗中抽象技術(shù)研究綜述[J];計算機工程與應(yīng)用;2006年33期

6 許翔;吳盡昭;林連南;陳劍鋒;;基于交互式馬爾可夫鏈的模型檢驗[J];計算機應(yīng)用;2008年07期

7 屈婉霞;李暾;郭陽;楊曉東;;一種高效的顯式模型檢驗方法[J];國防科技大學(xué)學(xué)報;2008年04期

8 譚亮;曾紅衛(wèi);;反例引導(dǎo)的模型檢驗工具的設(shè)計[J];計算機工程與設(shè)計;2009年22期

9 韓葆;蔡勉;;基于模型檢驗的軟件可信分析模型[J];計算機技術(shù)與發(fā)展;2012年10期

10 于慶梅;駱麗;;任務(wù)流模型檢驗的研究[J];電腦知識與技術(shù)(學(xué)術(shù)交流);2007年03期

中國重要會議論文全文數(shù)據(jù)庫 前4條

1 于慶梅;駱麗;;任務(wù)流模型檢驗的研究[A];中國通信集成電路技術(shù)與應(yīng)用研討會文集[C];2006年

2 宗群;竇立謙;孫連坤;劉文靜;;基于殘差分析方法的模型檢驗[A];第二十七屆中國控制會議論文集[C];2008年

3 曾紅衛(wèi);繆淮扣;;優(yōu)化基于模型檢驗的測試生成[A];第六屆中國測試學(xué)術(shù)會議論文集[C];2010年

4 葉俊民;張振方;王敬華;李蓉;;基于模型檢驗技術(shù)的源程序分析研究[A];2009年全國開放式分布與并行計算機學(xué)術(shù)會議論文集(上冊)[C];2009年

中國博士學(xué)位論文全文數(shù)據(jù)庫 前4條

1 董威;面向UML的模型檢驗研究[D];中國人民解放軍國防科學(xué)技術(shù)大學(xué);2002年

2 郭建;在數(shù)字系統(tǒng)設(shè)計中斷言驗證的研究[D];西安電子科技大學(xué);2008年

3 沈勝宇;模型檢驗的反例解釋[D];國防科學(xué)技術(shù)大學(xué);2005年

4 曾紅衛(wèi);Web應(yīng)用的驗證與測試方法研究[D];上海大學(xué);2008年

中國碩士學(xué)位論文全文數(shù)據(jù)庫 前10條

1 張振方;基于模型檢驗的軟件分析方法研究[D];華中師范大學(xué);2009年

2 崔曉旭;商業(yè)銀行評級模型檢驗系統(tǒng)的設(shè)計與實現(xiàn)[D];山東大學(xué);2012年

3 陳慶鋒;軟件漏洞模型檢驗技術(shù)的研究[D];華中科技大學(xué);2007年

4 劉霞;移動電子商務(wù)協(xié)議的模型檢驗分析與設(shè)計研究[D];桂林電子科技大學(xué);2006年

5 吳宏;基于LSC的模型檢驗研究與實現(xiàn)[D];國防科學(xué)技術(shù)大學(xué);2004年

6 顧益;結(jié)合模型檢驗的軟件失效模式與影響分析方法研究[D];南京航空航天大學(xué);2012年

7 劉超;基于模型檢驗的飛機系統(tǒng)安全性分析方法研究[D];南京航空航天大學(xué);2012年

8 張曦;基于WCET分析技術(shù)的程序?qū)崟r性模型檢驗方法研究[D];國防科學(xué)技術(shù)大學(xué);2011年

9 韓葆;基于模型檢驗的軟件可信性分析模型[D];北京工業(yè)大學(xué);2012年

10 楊志;基于吳方法的高層次模型檢驗方法研究[D];哈爾濱工程大學(xué);2008年

，

本文編號：1052487