發(fā)布時(shí)間：2017-11-06 05:02

  本文關(guān)鍵詞：基于MAS模型檢測(cè)與抽象的Web服務(wù)驗(yàn)證

  更多相關(guān)文章： Web服務(wù)組合 多主體系統(tǒng) 模型檢測(cè) 圖狀反例 抽象 精化

【摘要】：Web服務(wù)組合現(xiàn)已成為跨組織業(yè)務(wù)流程集成的關(guān)鍵技術(shù),然而在松耦合開(kāi)發(fā)模式和開(kāi)放的互聯(lián)網(wǎng)運(yùn)行環(huán)境下,其正確性、可靠性、安全性等可信性質(zhì)難以得到保證。為解決該問(wèn)題,提出一種Web服務(wù)組合形式化驗(yàn)證方法,將基于圖狀反例向?qū)У某橄笈c精化方法應(yīng)用于多主體系統(tǒng)(MAS)模型檢測(cè)工具(MCTK)中,大幅緩解模型檢測(cè)的狀態(tài)爆炸問(wèn)題,從理論上證明該驗(yàn)證方法的正確性。實(shí)驗(yàn)通過(guò)將銀行貸款風(fēng)險(xiǎn)評(píng)估系統(tǒng)轉(zhuǎn)換成MCTK描述的MAS,并對(duì)比抽象前后的模型檢測(cè)代價(jià),結(jié)果顯示,基于抽象的Web服務(wù)驗(yàn)證方法明顯優(yōu)于未采用抽象技術(shù)的驗(yàn)證方法。
【作者單位】： 華僑大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院;桂林電子科技大學(xué)廣西可信軟件重點(diǎn)實(shí)驗(yàn)室;
【基金】：國(guó)家自然科學(xué)基金資助面上項(xiàng)目(61170028) 華僑大學(xué)中青年教師科研提升計(jì)劃基金資助項(xiàng)目(ZQN-YX109) 華僑大學(xué)高層次人才科研啟動(dòng)基金資助項(xiàng)目(11BS108) 廣西可信軟件重點(diǎn)實(shí)驗(yàn)室基金資助項(xiàng)目(kx201323)
【分類(lèi)號(hào)】：TP393.09
【正文快照】： 中文引用格式:許興旺,駱翔宇.基于MAS模型檢測(cè)與抽象的Web服務(wù)驗(yàn)證[J].計(jì)算機(jī)工程,2015,41(3):26-31,36.1概述面向Web服務(wù)的軟件開(kāi)發(fā)已成為跨組織業(yè)務(wù)流程集成的關(guān)鍵技術(shù)。然而,單一Web服務(wù)功能有限,在多數(shù)情況下不能滿(mǎn)足用戶(hù)需求,因此出現(xiàn)將多個(gè)Web服務(wù)按某種特定組合集成為

【參考文獻(xiàn)】

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

1 駱翔宇;陳艷;;Web服務(wù)的形式化驗(yàn)證[J];計(jì)算機(jī)工程;2010年05期

2 駱翔宇;王昆;王鳳釵;;一種Web服務(wù)組合的認(rèn)知模型檢測(cè)方法[J];小型微型計(jì)算機(jī)系統(tǒng);2011年10期

【共引文獻(xiàn)】

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

1 俞東進(jìn);吳為;殷昱煜;閆大強(qiáng);劉志清;;基于模型檢測(cè)的服務(wù)規(guī)則路由正確性驗(yàn)證方法[J];電子科技大學(xué)學(xué)報(bào);2014年01期

2 高洪皓;繆淮扣;曾紅衛(wèi);;基于CEGAR的Web應(yīng)用驗(yàn)證[J];計(jì)算機(jī)學(xué)報(bào);2014年04期

3 Qian Junyan;Wu Juan;Zhao Lingzhong;Guo Yunchuan;;SUMMARIZATION OF BOOLEAN SATISFIABILITY VERIFICATION[J];Journal of Electronics(China);2014年03期

4 錢(qián)俊彥;趙嶺忠;蔡國(guó)永;;基于完備抽象解釋的性質(zhì)強(qiáng)保留抽象研究[J];計(jì)算機(jī)學(xué)報(bào);2014年08期

5 黃宏濤;王靜;葉海智;黃少濱;;基于惰性切片的線(xiàn)性時(shí)態(tài)邏輯性質(zhì)驗(yàn)證[J];吉林大學(xué)學(xué)報(bào)(工學(xué)版);2015年01期

6 化希耀;蘇博妮;陳立平;高賢強(qiáng);;模型檢測(cè)技術(shù)研究綜述[J];塔里木大學(xué)學(xué)報(bào);2013年04期

7 范大娟;黃志球;肖芳雄;彭煥峰;李雯睿;;一種需求驅(qū)動(dòng)的服務(wù)行為適配方法[J];四川大學(xué)學(xué)報(bào)(工程科學(xué)版);2014年02期

8 姚雪梅;艾穎;;基于SPIN求解狼和白菜過(guò)河問(wèn)題[J];銅仁職業(yè)技術(shù)學(xué)院學(xué)報(bào);2014年02期

9 趙會(huì)群;申寧;;Web服務(wù)組合編輯器的設(shè)計(jì)與實(shí)現(xiàn)[J];計(jì)算機(jī)技術(shù)與發(fā)展;2012年12期

10 彭蕾;;一種矛盾需求信息的建模方法[J];信息系統(tǒng)工程;2014年11期

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

1 田偉;模型驅(qū)動(dòng)的web應(yīng)用SQL注入安全漏洞滲透測(cè)試研究[D];南開(kāi)大學(xué);2012年

2 金洋;基于傳遞系統(tǒng)模型的在軌衛(wèi)星故障診斷方法研究[D];哈爾濱工業(yè)大學(xué);2013年

3 黃玉輝;配電網(wǎng)拓?fù)涞男问交磉_(dá)及其應(yīng)用[D];上海交通大學(xué);2013年

4 劉智;二進(jìn)制代碼級(jí)的漏洞攻擊檢測(cè)研究[D];電子科技大學(xué);2013年

5 駱超;混沌和異步布爾網(wǎng)絡(luò)中若干問(wèn)題的研究[D];大連理工大學(xué);2013年

6 袁敏;面向服務(wù)的業(yè)務(wù)事務(wù)建模與驗(yàn)證方法研究[D];南京航空航天大學(xué);2012年

7 高明;知識(shí)協(xié)同工作流建模、服務(wù)規(guī)劃和服務(wù)組合研究[D];東北財(cái)經(jīng)大學(xué);2013年

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

1 謝雨;Web服務(wù)合作關(guān)系模型研究[D];中南大學(xué);2012年

2 何霞;基于翻譯模式的BPEL到LOTOS映射方法研究[D];北方工業(yè)大學(xué);2013年

3 水晶;GSM-R在信號(hào)集中監(jiān)測(cè)系統(tǒng)中的應(yīng)用研究[D];蘭州交通大學(xué);2013年

4 王杰;USB3.0設(shè)備控制器IP核控制端點(diǎn)的RTL功能驗(yàn)證[D];合肥工業(yè)大學(xué);2013年

5 張壹;C語(yǔ)言應(yīng)用程序的靜態(tài)漏洞檢測(cè)[D];華中科技大學(xué);2013年

6 萬(wàn)季;嵌入式軟件缺陷檢測(cè)的測(cè)試用例生成與排序研究[D];杭州電子科技大學(xué);2014年

7 胡瀚月;面向C語(yǔ)言代碼的規(guī)則檢測(cè)工具研究[D];蘭州理工大學(xué);2014年

8 陳娟娟;基于雙格的多值模型精化關(guān)系及對(duì)稱(chēng)化簡(jiǎn)[D];南京航空航天大學(xué);2014年

9 許興旺;基于多智能體系統(tǒng)模型檢測(cè)與抽象技術(shù)的Web服務(wù)組合驗(yàn)證[D];華僑大學(xué);2014年

10 屈麗;基于QoS證據(jù)數(shù)據(jù)庫(kù)的服務(wù)合作關(guān)系研究[D];中南大學(xué);2014年

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

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

1 駱翔宇;蘇開(kāi)樂(lè);楊晉吉;;有界模型檢測(cè)同步多智體系統(tǒng)的時(shí)態(tài)認(rèn)知邏輯[J];軟件學(xué)報(bào);2006年12期

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

1 駱翔宇;多智能體系統(tǒng)的符號(hào)模型檢測(cè)[D];中山大學(xué);2006年

【相似文獻(xiàn)】

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

1 鄺宏斌;羅貴明;;并行軟件模型檢測(cè)[J];計(jì)算機(jī)工程;2008年19期

2 周立青;楊晉吉;;樂(lè)觀(guān)合同簽訂協(xié)議的模型檢測(cè)分析[J];計(jì)算機(jī)工程;2011年07期

3 周從華;劉志鋒;;具有過(guò)去時(shí)態(tài)算子的計(jì)算樹(shù)邏輯模型檢測(cè)[J];計(jì)算機(jī)工程;2007年22期

4 陳振宇;陶志紅;KLEINE BüNING Hans;王立福;;變量極小不可滿(mǎn)足在模型檢測(cè)中的應(yīng)用(英文)[J];軟件學(xué)報(bào);2008年01期

5 陳清亮;朱可宜;;多智能體協(xié)同的認(rèn)知規(guī)范模型檢測(cè)算法[J];中山大學(xué)學(xué)報(bào)(自然科學(xué)版);2009年01期

6 馮慶奎;;基于一階遷移系統(tǒng)的限界模型檢測(cè)工具實(shí)現(xiàn)[J];計(jì)算機(jī)工程與設(shè)計(jì);2010年01期

7 駱翔宇;蘇開(kāi)樂(lè);顧明;;一種求解認(rèn)知難題的模型檢測(cè)方法[J];計(jì)算機(jī)學(xué)報(bào);2010年03期

8 韋林;古天龍;常亮;;基于模型檢測(cè)的命題動(dòng)態(tài)邏輯規(guī)劃[J];桂林電子科技大學(xué)學(xué)報(bào);2010年02期

9 劉劍,林惠民;傳值進(jìn)程模型檢測(cè)中診斷信息的生成[J];軟件學(xué)報(bào);2003年01期

10 肖健宇;張德運(yùn);鄭衛(wèi)斌;張勇;;程序條件化用于軟件模型檢測(cè)中的狀態(tài)空間縮減[J];西安交通大學(xué)學(xué)報(bào);2006年04期

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

1 高靜;曹子寧;;基于空間邏輯和計(jì)算樹(shù)邏輯的模型檢測(cè)[A];2009年中國(guó)高校通信類(lèi)院系學(xué)術(shù)研討會(huì)論文集[C];2009年

2 許梅;曹子寧;;基于謂詞μ演算和空間邏輯的模型檢測(cè)算法研究[A];2009年中國(guó)高校通信類(lèi)院系學(xué)術(shù)研討會(huì)論文集[C];2009年

3 何青;駱翔宇;蘇開(kāi)樂(lè);;對(duì)弈必勝策略的符號(hào)化模型檢測(cè)[A];2006年全國(guó)理論計(jì)算機(jī)科學(xué)學(xué)術(shù)年會(huì)論文集[C];2006年

4 王飛明;胡元闖;董榮勝;;模型檢測(cè)中狀態(tài)爆炸及其優(yōu)化策略研究[A];廣西計(jì)算機(jī)學(xué)會(huì)2008年年會(huì)論文集[C];2008年

5 陳道喜;張廣泉;陳冬火;;NSPK協(xié)議的Spin模型檢測(cè)[A];2008年全國(guó)開(kāi)放式分布與并行計(jì)算機(jī)學(xué)術(shù)會(huì)議論文集(下冊(cè))[C];2008年

6 邢立國(guó);張光甫;劉薇;胥維昌;金一和;;人皮膚模型評(píng)價(jià)殺菌類(lèi)農(nóng)藥腐蝕/刺激性研究[A];2014線(xiàn)粒體毒性與基于毒性通路的安全性評(píng)價(jià)新策略學(xué)術(shù)研討會(huì)暨中國(guó)毒理學(xué)會(huì)毒理學(xué)替代法與轉(zhuǎn)化毒理學(xué)專(zhuān)業(yè)委員會(huì)成立大會(huì)論文集[C];2014年

7 張明玉;;我國(guó)對(duì)外開(kāi)放、通貨膨脹與經(jīng)濟(jì)增長(zhǎng)相關(guān)關(guān)系的模型檢測(cè)[A];面向21世紀(jì)的科技進(jìn)步與社會(huì)經(jīng)濟(jì)發(fā)展（下冊(cè)）[C];1999年

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

1 江華;界程演算模型檢測(cè)[D];貴州大學(xué);2008年

2 林榮德;移動(dòng)界程演算及模型檢測(cè)應(yīng)用的關(guān)鍵問(wèn)題研究[D];華南理工大學(xué);2010年

3 劉劍;傳值進(jìn)程與移動(dòng)進(jìn)程的模型檢測(cè)方法[D];中國(guó)科學(xué)院研究生院（軟件研究所）;2005年

4 劉志鋒;模型檢測(cè)中關(guān)鍵技術(shù)的研究及其應(yīng)用[D];南京大學(xué);2011年

5 朱維軍;時(shí)間區(qū)間時(shí)序邏輯模型檢測(cè)：理論、算法及應(yīng)用[D];西安電子科技大學(xué);2011年

6 陳冬火;超協(xié)調(diào)時(shí)序邏輯及其模型檢測(cè)方法[D];中國(guó)科學(xué)院研究生院（成都計(jì)算機(jī)應(yīng)用研究所）;2006年

7 田聰;命題投影時(shí)序邏輯的判定性、復(fù)雜性、表達(dá)性及模型檢測(cè)[D];西安電子科技大學(xué);2010年

8 黃宏濤;基于懶惰切片的模型檢測(cè)技術(shù)研究[D];哈爾濱工程大學(xué);2012年

9 劉金卓;基于符號(hào)化模型檢測(cè)的軟件演化過(guò)程模型驗(yàn)證[D];云南大學(xué);2013年

10 吳駿;多Agent聯(lián)盟規(guī)范系統(tǒng)研究[D];南京大學(xué);2011年

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

1 張衍志;符號(hào)化模型檢測(cè)算法的研究[D];吉林大學(xué);2009年

2 黎吾平;模型檢測(cè)在軟件方面的應(yīng)用[D];吉林大學(xué);2008年

3 吳小娟;并行完備模型檢測(cè)技術(shù)的研究[D];電子科技大學(xué);2013年

4 姜志敏;模型檢測(cè)在配置中的應(yīng)用[D];吉林大學(xué);2010年

5 金怡愛(ài);基于模型檢測(cè)方法的規(guī)劃[D];吉林大學(xué);2005年

6 施小純;基于反例搜索的啟發(fā)式模型檢測(cè)算法的研究[D];中國(guó)科學(xué)院研究生院（軟件研究所）;2004年

7 陳亞軍;模型檢測(cè)在安全協(xié)議形式化驗(yàn)證中的應(yīng)用[D];電子科技大學(xué);2012年

8 高靜;面向環(huán)境演算系統(tǒng)的模型檢測(cè)算法的研究[D];南京航空航天大學(xué);2009年

9 龔愛(ài)民;基于模型檢測(cè)的模型驅(qū)動(dòng)式開(kāi)發(fā)系統(tǒng)的設(shè)計(jì)與實(shí)現(xiàn)[D];華東師范大學(xué);2008年

10 黃丫;基于模型檢測(cè)的可診斷性的形式化檢驗(yàn)研究[D];吉林大學(xué);2006年

，

本文編號(hào)：1147425