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

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

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

【參考文獻】

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

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

2 顏炯;王戟;陳火旺;;基于模型的軟件測試綜述[J];計算機科學;2004年02期

3 曾一;張利武;張元平;袁綱;李強;;一種基于活動圖的并發(fā)軟件測試線索生成方法[J];計算機科學;2007年12期

【共引文獻】

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

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

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

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

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

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

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

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

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

9 呂金和;;軟件安全性測試研究[J];計算機安全;2010年08期

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

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

1 馮亞冬;熊波;;基于適航認證的FADEC軟件自動化測試平臺的研究[A];2011航空試驗測試技術學術交流會論文集[C];2010年

2 陳振華;王峰;;操作剖面與軟件可靠性[A];2006年全國理論計算機科學學術年會論文集[C];2006年

3 楊春暉;李冬;熊婧;;一種基于任務模塊的實時軟件可靠性評價模型[A];2010第十五屆可靠性學術年會論文集[C];2010年

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

5 孫晶;趙會群;馬云峰;;基于TTCN的手機游戲軟件測試方法研究[A];第四屆中國測試學術會議論文集[C];2006年

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

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

2 曾凡平;軟件漏洞測試若干問題研究[D];中國科學技術大學;2009年

3 錢思佑;圖形用戶界面測試中相關問題研究[D];中國科學技術大學;2010年

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

5 李麗;航天相機主控軟件測試用例自動生成技術的研究[D];中國科學院研究生院（長春光學精密機械與物理研究所）;2010年

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

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

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

1 張作梅;教育軟件自動測試系統(tǒng)設計[D];華東師范大學;2010年

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

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

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

5 王新紅;構件軟件黑盒測試研究及應用[D];華北電力大學;2011年

6 郭麗娟;基于即時驗證的嵌入式軟件驗證技術研究[D];南京航空航天大學;2010年

7 馮亞冬;適航認證的FADEC軟件自動測試平臺的研究[D];上海交通大學;2011年

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

9 宋建斌;城市軌道交通運營管理系統(tǒng)測試與評價方法研究[D];蘇州大學;2011年

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

【二級參考文獻】

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

1 顏炯;王戟;陳火旺;;基于模型的軟件測試綜述[J];計算機科學;2004年02期

2 梅宏;王千祥;張路;王戟;;軟件分析技術進展[J];計算機學報;2009年09期

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

4 趙煒;曾一;張利武;;基于UML活動圖生成功能測試線索[J];計算機工程與設計;2006年22期

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

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

【相似文獻】

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

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

2 蘇繼斌;肖宗水;肖迎杰;;網(wǎng)絡風險評估滲透圖生成算法的設計[J];計算機工程與應用;2010年17期

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

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

5 陳國彬;任強;張廣泉;;一種基于抽象與精化技術的Web服務組合驗證方法[J];計算機工程與科學;2011年09期

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

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

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

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

10 杜彥華;范玉順;李喜彤;;基于模塊化可達圖的服務組合驗證及BPEL代碼生成[J];軟件學報;2010年08期

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

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

2 逄建;張廣勝;于朝萍;;基于Petri網(wǎng)的網(wǎng)絡系統(tǒng)脆弱性評估[A];第十九次全國計算機安全學術交流會論文集[C];2004年

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

，

本文編號：890001