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

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

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

【參考文獻(xiàn)】

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

1 林惠民,張文輝;模型檢測(cè):理論、方法與應(yīng)用[J];電子學(xué)報(bào);2002年S1期

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

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

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

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

【共引文獻(xiàn)】

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

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

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

3 張O，

本文編號(hào)：1001774