本文關(guān)鍵詞：基于抽象和組合方法的網(wǎng)絡協(xié)議驗證

  更多相關(guān)文章： Kripke結(jié)構(gòu) 狀態(tài)爆炸 組合抽象模型 LTL模型檢測

【摘要】：由于模型檢測存在狀態(tài)爆炸問題,多主體的網(wǎng)絡協(xié)議組合模型檢測往往難以進行。為了緩解該問題,分析了通信主體數(shù)量增加對狀態(tài)數(shù)量的影響,提出了組合式的抽象驗證方法。首先根據(jù)所需驗證的LTL性質(zhì),建立各個通信主體的Kripke結(jié)構(gòu),再對該Kripke結(jié)構(gòu)進行抽象;然后組合抽象模型;最后運用Spin對組合抽象模型進行檢驗。為驗證該方法的有效性,對NSPK協(xié)議進行了檢測,結(jié)果表明,該方法所需的狀態(tài)空間向量長度、搜索深度、存貯和遍歷的狀態(tài)數(shù)都有明顯減少,有利于緩解狀態(tài)爆炸問題。
【作者單位】： 蘇州技師學院;蘇州大學計算機科學與技術(shù)學院;重慶工商大學融智學院;
【關(guān)鍵詞】： Kripke結(jié)構(gòu) 狀態(tài)爆炸 組合抽象模型 LTL模型檢測
【基金】：江蘇省自然科學基金(BK2011281) 蘇州市應用基礎研究計劃(SYG201241) 江蘇省普通高校研究生科研創(chuàng)新計劃(CXLX13_820) 重慶市教委科學技術(shù)研究項目(KJ133103)資助
【分類號】：TP393.04;TP311.52
【正文快照】： 到稿日期:2014-06-30返修日期:2014-10-04本文受江蘇省自然科學基金(BK2011281),蘇州市應用基礎研究計劃(SYG201241),江蘇省普通高校研究生科研創(chuàng)新計劃(CXLX13_820),重慶市教委科學技術(shù)研究項目(KJ133103)資助。模型檢測是一種驗證有限狀態(tài)并發(fā)系統(tǒng)的自動化技術(shù)[1]。首先要建

【參考文獻】

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

1 林惠民,張文輝;模型檢測:理論、方法與應用[J];電子學報;2002年S1期

2 劉志鋒;孫博;周從華;;概率實時時態(tài)認知邏輯模型檢測中抽象技術(shù)的研究[J];電子學報;2013年07期

3 呂威;黃志球;陳哲;闞雙龍;魏歐;;ESpin:基于SPIN的Eclipse模型檢測環(huán)境[J];計算機工程與應用;2013年07期

4 曾紅衛(wèi);繆淮扣;;構(gòu)件組合的抽象精化驗證[J];軟件學報;2008年05期

5 高建華;蔣穎;;基于余歸納的最小Kripke結(jié)構(gòu)的求解[J];軟件學報;2014年01期

【共引文獻】

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

1 李忠慧;張廣泉;;基于UPPAAL的NS密碼協(xié)議模型檢測分析[J];重慶師范大學學報(自然科學版);2009年04期

2 梁陳良;聶長海;徐寶文;陳振宇;;一種基于模型檢驗的類測試用例生成方法[J];東南大學學報(自然科學版);2007年05期

3 張O，

本文編號：1001774