本文關(guān)鍵詞：一種針對(duì)CP-nets并發(fā)模型的驗(yàn)證方法

  更多相關(guān)文章： 模型驗(yàn)證 化簡(jiǎn) 抽象 狀態(tài)爆炸

【摘要】：狀態(tài)爆炸問題導(dǎo)致CP-nets并發(fā)模型的正確性驗(yàn)證工作十分困難。提出了基于并發(fā)屬性的模型化簡(jiǎn)方法和基于功能組合的模型抽象方法,用于對(duì)模型進(jìn)行處理,移去與并發(fā)屬性不相關(guān)的模型元素,提升模型的抽象層次,使模型狀態(tài)空間規(guī)模得到顯著降低,并在并發(fā)屬性相關(guān)行為上與原模型保持一致;在處理后模型中運(yùn)用狀態(tài)空間分析、模型檢測(cè)等驗(yàn)證方法完成模型驗(yàn)證,針對(duì)驗(yàn)證得出的模型錯(cuò)誤,通過處理前后模型的對(duì)照關(guān)系在原模型中進(jìn)行改正。這在一定程度上避免了狀態(tài)爆炸問題并實(shí)現(xiàn)了模型驗(yàn)證。通過將上述方法應(yīng)用于HMIPv6協(xié)議模型,驗(yàn)證了其有效性。
【作者單位】： 內(nèi)蒙古大學(xué)計(jì)算機(jī)學(xué)院;
【關(guān)鍵詞】： 模型驗(yàn)證 化簡(jiǎn) 抽象 狀態(tài)爆炸
【基金】：國(guó)家自然科學(xué)基金資助項(xiàng)目(61262017);國(guó)家自然科學(xué)基金資助項(xiàng)目(61163011) 內(nèi)蒙古自然科學(xué)基金資助項(xiàng)目(2012MS0922);內(nèi)蒙古自然科學(xué)基金資助項(xiàng)目(2011MS0912)資助
【分類號(hào)】：TP393.04
【正文快照】： 1引言在現(xiàn)實(shí)世界中,并發(fā)系統(tǒng)是無處不在、不可或缺的;在計(jì)算機(jī)軟件領(lǐng)域中,隨著互聯(lián)網(wǎng)的日益發(fā)展,并發(fā)軟件也成為了最為主流的軟件形式之一。例如,包括移動(dòng)網(wǎng)絡(luò)協(xié)議在內(nèi)的各種網(wǎng)絡(luò)協(xié)議、包括云計(jì)算軟件在內(nèi)的各類網(wǎng)絡(luò)軟件都具有并發(fā)性特點(diǎn)。并發(fā)系統(tǒng)已成為研究熱點(diǎn)之一,例如,關(guān)

【參考文獻(xiàn)】

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

1 孫濤;葉新銘;劉靖;楊蒙;;一種基于CPN的協(xié)議測(cè)試序列生成方法[J];解放軍理工大學(xué)學(xué)報(bào)(自然科學(xué)版);2012年02期

2 顏炯;王戟;陳火旺;;基于模型的軟件測(cè)試綜述[J];計(jì)算機(jī)科學(xué);2004年02期

3 曾一;張利武;張?jiān)?袁綱;李強(qiáng);;一種基于活動(dòng)圖的并發(fā)軟件測(cè)試線索生成方法[J];計(jì)算機(jī)科學(xué);2007年12期

【共引文獻(xiàn)】

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

1 陳闖;;基于UML的網(wǎng)站設(shè)計(jì)與實(shí)現(xiàn)——以畢節(jié)學(xué)院人事處網(wǎng)站為例[J];畢節(jié)學(xué)院學(xué)報(bào);2009年04期

2 陳穎慧;邱雪松;劉益暢;唐凡;高志鵬;;基于模型的Web Service性能測(cè)試方法[J];北京郵電大學(xué)學(xué)報(bào);2009年S1期

3 田志民;林奇;羅雪萊;孟慶浩;;一種面向國(guó)防工業(yè)的應(yīng)用軟件漏洞檢測(cè)方法[J];保密科學(xué)技術(shù);2012年01期

4 牟小玲;丁曉明;張望;;基于Petri網(wǎng)的測(cè)試用例生成研究進(jìn)展[J];重慶交通大學(xué)學(xué)報(bào)(自然科學(xué)版);2012年01期

5 雷航;馬成功;;Markov模型的軟件可靠性測(cè)試充分性問題的研究[J];電子科技大學(xué)學(xué)報(bào);2010年01期

6 嚴(yán)海軍;;基于UML的江蘇省藥物研究所網(wǎng)站分析設(shè)計(jì)[J];電腦知識(shí)與技術(shù);2011年35期

7 楊廣華;齊璇;施寅生;;基于威脅模型的軟件安全性測(cè)試[J];計(jì)算機(jī)安全;2010年02期

8 呂金和;;由指針和數(shù)組帶來的軟件安全性缺陷[J];計(jì)算機(jī)安全;2010年05期

9 呂金和;;軟件安全性測(cè)試研究[J];計(jì)算機(jī)安全;2010年08期

10 鄭薇瑋;;基于模型的軟件測(cè)試新工具——UPPAAL TRON[J];福建廣播電視大學(xué)學(xué)報(bào);2010年06期

中國(guó)重要會(huì)議論文全文數(shù)據(jù)庫 前5條

1 馮亞冬;熊波;;基于適航認(rèn)證的FADEC軟件自動(dòng)化測(cè)試平臺(tái)的研究[A];2011航空試驗(yàn)測(cè)試技術(shù)學(xué)術(shù)交流會(huì)論文集[C];2010年

2 陳振華;王峰;;操作剖面與軟件可靠性[A];2006年全國(guó)理論計(jì)算機(jī)科學(xué)學(xué)術(shù)年會(huì)論文集[C];2006年

3 楊春暉;李冬;熊婧;;一種基于任務(wù)模塊的實(shí)時(shí)軟件可靠性評(píng)價(jià)模型[A];2010第十五屆可靠性學(xué)術(shù)年會(huì)論文集[C];2010年

4 陳穎慧;邱雪松;劉益暢;唐凡;高志鵬;;基于模型的Web Service性能測(cè)試方法[A];中國(guó)通信學(xué)會(huì)通信軟件技術(shù)委員會(huì)2009年學(xué)術(shù)會(huì)議論文集[C];2009年

5 孫晶;趙會(huì)群;馬云峰;;基于TTCN的手機(jī)游戲軟件測(cè)試方法研究[A];第四屆中國(guó)測(cè)試學(xué)術(shù)會(huì)議論文集[C];2006年

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

1 劉振宇;服務(wù)網(wǎng)格環(huán)境中場(chǎng)景測(cè)試的關(guān)鍵技術(shù)研究[D];復(fù)旦大學(xué);2010年

2 曾凡平;軟件漏洞測(cè)試若干問題研究[D];中國(guó)科學(xué)技術(shù)大學(xué);2009年

3 錢思佑;圖形用戶界面測(cè)試中相關(guān)問題研究[D];中國(guó)科學(xué)技術(shù)大學(xué);2010年

4 張毅坤;COTS構(gòu)件集成軟件系統(tǒng)的測(cè)試方法研究[D];西安理工大學(xué);2008年

5 李麗;航天相機(jī)主控軟件測(cè)試用例自動(dòng)生成技術(shù)的研究[D];中國(guó)科學(xué)院研究生院（長(zhǎng)春光學(xué)精密機(jī)械與物理研究所）;2010年

6 丁曉明;基于構(gòu)件的軟件開發(fā)關(guān)鍵問題研究[D];西南大學(xué);2012年

7 孫濤;基于CP-nets模型的并行軟件測(cè)試方法研究[D];內(nèi)蒙古大學(xué);2012年

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

1 張作梅;教育軟件自動(dòng)測(cè)試系統(tǒng)設(shè)計(jì)[D];華東師范大學(xué);2010年

2 靖焱林;基于UML-XML的車載設(shè)備測(cè)試用例生成方法研究和實(shí)現(xiàn)[D];北京交通大學(xué);2011年

3 勞陽輝;AOP代碼中幾種特定缺陷的軟件測(cè)試方法[D];昆明理工大學(xué);2010年

4 黃X;軟件缺陷分析及質(zhì)量度量系統(tǒng)的設(shè)計(jì)與實(shí)現(xiàn)[D];西安電子科技大學(xué);2011年

5 王新紅;構(gòu)件軟件黑盒測(cè)試研究及應(yīng)用[D];華北電力大學(xué);2011年

6 郭麗娟;基于即時(shí)驗(yàn)證的嵌入式軟件驗(yàn)證技術(shù)研究[D];南京航空航天大學(xué);2010年

7 馮亞冬;適航認(rèn)證的FADEC軟件自動(dòng)測(cè)試平臺(tái)的研究[D];上海交通大學(xué);2011年

8 姜喜梅;基于馬爾可夫鏈的單證關(guān)系建模的研究與實(shí)現(xiàn)[D];哈爾濱工程大學(xué);2011年

9 宋建斌;城市軌道交通運(yùn)營(yíng)管理系統(tǒng)測(cè)試與評(píng)價(jià)方法研究[D];蘇州大學(xué);2011年

10 李偉;呼叫中心系統(tǒng)性能測(cè)試和分析[D];北京郵電大學(xué);2012年

【二級(jí)參考文獻(xiàn)】

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

1 顏炯;王戟;陳火旺;;基于模型的軟件測(cè)試綜述[J];計(jì)算機(jī)科學(xué);2004年02期

2 梅宏;王千祥;張路;王戟;;軟件分析技術(shù)進(jìn)展[J];計(jì)算機(jī)學(xué)報(bào);2009年09期

3 顧慶,陳道蓄,謝立,韓杰,孫鐘秀;基于有限狀態(tài)進(jìn)程的事件約束定義[J];軟件學(xué)報(bào);2002年11期

4 趙煒;曾一;張利武;;基于UML活動(dòng)圖生成功能測(cè)試線索[J];計(jì)算機(jī)工程與設(shè)計(jì);2006年22期

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

1 趙煒;基于UML提取系統(tǒng)測(cè)試線索方法的研究[D];重慶大學(xué);2006年

【相似文獻(xiàn)】

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

1 吳昌;肖美華;羅敏;劉俏威;熊昊;;安全協(xié)議驗(yàn)證模型的高效自動(dòng)生成[J];計(jì)算機(jī)工程與應(yīng)用;2010年02期

2 蘇繼斌;肖宗水;肖迎杰;;網(wǎng)絡(luò)風(fēng)險(xiǎn)評(píng)估滲透圖生成算法的設(shè)計(jì)[J];計(jì)算機(jī)工程與應(yīng)用;2010年17期

3 苘大鵬;周淵;楊武;楊永田;;用于評(píng)估網(wǎng)絡(luò)整體安全性的攻擊圖生成方法[J];通信學(xué)報(bào);2009年03期

4 蘇繼斌;肖宗水;肖迎杰;;基于滲透圖的網(wǎng)絡(luò)弱點(diǎn)分析與研究[J];計(jì)算機(jī)工程;2009年23期

5 陳國(guó)彬;任強(qiáng);張廣泉;;一種基于抽象與精化技術(shù)的Web服務(wù)組合驗(yàn)證方法[J];計(jì)算機(jī)工程與科學(xué);2011年09期

6 劉培,周明天;基于串空間的認(rèn)證協(xié)議分析[J];實(shí)驗(yàn)科學(xué)與技術(shù);2005年03期

7 王之梁;吳建平;尹霞;施新剛;;基于MSC測(cè)試目的的協(xié)議互操作性測(cè)試生成[J];北京郵電大學(xué)學(xué)報(bào);2006年S1期

8 苘大鵬;張冰;周淵;楊武;楊永田;;一種深度優(yōu)先的攻擊圖生成方法[J];吉林大學(xué)學(xué)報(bào)(工學(xué)版);2009年02期

9 舒挺;孫守遷;王海寧;徐偉強(qiáng);李文書;;啟發(fā)式探索的協(xié)議測(cè)試序列生成[J];北京郵電大學(xué)學(xué)報(bào);2009年06期

10 杜彥華;范玉順;李喜彤;;基于模塊化可達(dá)圖的服務(wù)組合驗(yàn)證及BPEL代碼生成[J];軟件學(xué)報(bào);2010年08期

中國(guó)重要會(huì)議論文全文數(shù)據(jù)庫 前2條

1 謝朝海;陶然;李志勇;李繼勇;;基于弱點(diǎn)相關(guān)性的網(wǎng)絡(luò)安全性分析方法[A];全國(guó)網(wǎng)絡(luò)與信息安全技術(shù)研討會(huì)論文集（上冊(cè)）[C];2007年

2 逄建;張廣勝;于朝萍;;基于Petri網(wǎng)的網(wǎng)絡(luò)系統(tǒng)脆弱性評(píng)估[A];第十九次全國(guó)計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)論文集[C];2004年

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

1 王玉英;基于賦時(shí)有色Petri網(wǎng)的Web服務(wù)組合建模驗(yàn)證與測(cè)試技術(shù)研究[D];西安電子科技大學(xué);2012年

2 楊學(xué)紅;BPEL流程的故障模式及其靜態(tài)分析技術(shù)的研究[D];北京郵電大學(xué);2011年

3 李華;基于屬性的網(wǎng)絡(luò)協(xié)議建模與互操作性測(cè)試方法研究[D];內(nèi)蒙古大學(xué);2010年

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

1 劉鵬;面向存儲(chǔ)的正則表達(dá)式匹配算法研究[D];解放軍信息工程大學(xué);2010年

2 蘇繼斌;基于滲透圖的網(wǎng)絡(luò)弱點(diǎn)評(píng)估研究[D];山東大學(xué);2009年

3 井維亮;基于攻擊圖的網(wǎng)絡(luò)安全評(píng)估技術(shù)研究[D];哈爾濱工程大學(xué);2008年

4 吳昌;網(wǎng)絡(luò)安全協(xié)議的高效分析系統(tǒng)[D];南昌大學(xué);2008年

5 肖露娟;Web服務(wù)組合性能分析[D];浙江理工大學(xué);2010年

6 鄧珍榮;基于串空間模型的協(xié)議驗(yàn)證技術(shù)研究[D];廣西大學(xué);2005年

7 朱澤智;網(wǎng)絡(luò)內(nèi)容審計(jì)系統(tǒng)的研究與實(shí)現(xiàn)[D];北京郵電大學(xué);2010年

8 殷珍珍;基于正則表達(dá)式的多模式匹配算法研究[D];杭州電子科技大學(xué);2012年

9 王煥云;面向深度數(shù)據(jù)包檢測(cè)的正則表達(dá)式匹配算法研究[D];湖南大學(xué);2012年

10 譚志華;網(wǎng)絡(luò)認(rèn)證協(xié)議的高效模型檢測(cè)研究[D];湖南大學(xué);2011年

，

本文編號(hào)：890001