【摘要】：針對(duì)web服務(wù)模型檢測(cè)應(yīng)用中,傳統(tǒng)的有限狀態(tài)機(jī)的組合方式無(wú)法保證Web組合服務(wù)的正確性問(wèn)題,提出一種基于可滿足性模理論(satisfiability modulo theories,SMT)的非集中自動(dòng)機(jī)的web服務(wù)模型檢測(cè)算法。利用SMT對(duì)時(shí)間自動(dòng)機(jī)進(jìn)行有界模型檢測(cè),將時(shí)間自動(dòng)機(jī)模型直接轉(zhuǎn)換成SMT可識(shí)別的邏輯公式,并進(jìn)行求解;利用所提SMT時(shí)間自動(dòng)機(jī)理論,實(shí)現(xiàn)對(duì)雇員出差安排組合web服務(wù)進(jìn)行建模和驗(yàn)證;通過(guò)實(shí)例分析,驗(yàn)證了算法在解除路徑死鎖及網(wǎng)絡(luò)參數(shù)指標(biāo)優(yōu)化上的有效性。
[Abstract]:In order to solve the problem that the traditional finite state machine (FSM) composition method can not guarantee the correctness of Web composition services in web service model detection applications, a web service model detection algorithm based on satisfiability module theory (satisfiability modulo theories,SMT) is proposed. The bounded model of time automata is checked by SMT, and the time automaton model is transformed directly into the logical formula recognizable by SMT and solved, and the theory of SMT time automaton is used to solve the problem. The modeling and verification of employee travel arrangement composition web service is realized, and the effectiveness of the algorithm in the optimization of path deadlock and network parameter index is verified by an example analysis.
【作者單位】： 欽州學(xué)院人文學(xué)院;廣西科技大學(xué)軟件學(xué)院;
【分類號(hào)】：TP393.09

【相似文獻(xiàn)】

相關(guān)期刊論文 前10條

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

2 徐暢;劉吉鋒;孫吉貴;;基于經(jīng)典邏輯的安全協(xié)議模型檢測(cè)方法[J];計(jì)算機(jī)科學(xué);2008年06期

3 鈕俊;曾國(guó)蓀;王偉;;基于模型檢測(cè)的時(shí)間空間性能驗(yàn)證方法[J];計(jì)算機(jī)學(xué)報(bào);2010年09期

4 吉猛;胡克瑾;;基于模型檢測(cè)的電子商務(wù)鑒證技術(shù)[J];陜西師范大學(xué)學(xué)報(bào)(自然科學(xué)版);2006年04期

5 唐鄭熠;許道云;王曉峰;王正才;;基于模型檢測(cè)技術(shù)的語(yǔ)義Web服務(wù)自動(dòng)組合[J];吉林大學(xué)學(xué)報(bào)(工學(xué)版);2013年02期

6 陳小峰;馮登國(guó);;可信密碼模塊的模型檢測(cè)分析[J];通信學(xué)報(bào);2010年01期

7 呂審;;基于模型檢測(cè)的密碼協(xié)議安全性的實(shí)際應(yīng)用[J];電腦知識(shí)與技術(shù);2011年09期

8 張冬梅,馬華東,高大永;基于Uppaal的移動(dòng)IPv6協(xié)議的模型檢測(cè)[J];北京郵電大學(xué)學(xué)報(bào);2005年04期

9 馬懷磊;郭華;莊雷;;基于模型檢測(cè)的不可靠環(huán)境下電子商務(wù)協(xié)議分析[J];計(jì)算機(jī)工程與科學(xué);2007年10期

10 劉如娟;戴桂蘭;胡長(zhǎng)軍;白曉穎;;Web服務(wù)的模型檢測(cè)技術(shù)探討[J];小型微型計(jì)算機(jī)系統(tǒng);2007年11期

相關(guān)博士學(xué)位論文 前1條

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

相關(guān)碩士學(xué)位論文 前10條

1 于文光;一種基于BDD的語(yǔ)義Web服務(wù)組裝規(guī)劃器的設(shè)計(jì)與實(shí)現(xiàn)[D];北京大學(xué);2008年

2 郭華;基于模型檢測(cè)的電子商務(wù)協(xié)議形式化驗(yàn)證方法研究[D];鄭州大學(xué);2006年

3 王敏飛;模型檢測(cè)在安全協(xié)議驗(yàn)證中的研究與應(yīng)用[D];南京航空航天大學(xué);2009年

4 劉吉鋒;一個(gè)新的基于SAT方法的安全協(xié)議模型檢測(cè)算法[D];吉林大學(xué);2007年

5 陳艷;基于時(shí)態(tài)認(rèn)知邏輯的Web服務(wù)模型檢測(cè)[D];桂林電子科技大學(xué);2009年

6 郭肇毅;基于模型檢測(cè)的形式化協(xié)議驗(yàn)證[D];電子科技大學(xué);2012年

7 萬(wàn)子龍;基于模型檢測(cè)的SET協(xié)議形式化驗(yàn)證與改進(jìn)[D];南昌大學(xué);2014年

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

9 黃瑛;SET協(xié)議支付過(guò)程分析及模型檢測(cè)[D];貴州大學(xué);2006年

10 阮小黎;基于模型檢測(cè)的C語(yǔ)言安全信息流研究[D];清華大學(xué);2007年

，

本文編號(hào)：2200381