【摘要】：針對web服務(wù)模型檢測應(yīng)用中,傳統(tǒng)的有限狀態(tài)機(jī)的組合方式無法保證Web組合服務(wù)的正確性問題,提出一種基于可滿足性模理論(satisfiability modulo theories,SMT)的非集中自動機(jī)的web服務(wù)模型檢測算法。利用SMT對時間自動機(jī)進(jìn)行有界模型檢測,將時間自動機(jī)模型直接轉(zhuǎn)換成SMT可識別的邏輯公式,并進(jìn)行求解;利用所提SMT時間自動機(jī)理論,實現(xiàn)對雇員出差安排組合web服務(wù)進(jì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é)院;
【分類號】：TP393.09

【相似文獻(xiàn)】

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

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

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

3 鈕俊;曾國蓀;王偉;;基于模型檢測的時間空間性能驗證方法[J];計算機(jī)學(xué)報;2010年09期

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

，

本文編號：2200381