【摘要】：針對web服務模型檢測應用中,傳統(tǒng)的有限狀態(tài)機的組合方式無法保證Web組合服務的正確性問題,提出一種基于可滿足性模理論(satisfiability modulo theories,SMT)的非集中自動機的web服務模型檢測算法。利用SMT對時間自動機進行有界模型檢測,將時間自動機模型直接轉(zhuǎn)換成SMT可識別的邏輯公式,并進行求解;利用所提SMT時間自動機理論,實現(xiàn)對雇員出差安排組合web服務進行建模和驗證;通過實例分析,驗證了算法在解除路徑死鎖及網(wǎng)絡參數(shù)指標優(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.
【作者單位】： 欽州學院人文學院;廣西科技大學軟件學院;
【分類號】：TP393.09

【相似文獻】

相關期刊論文 前10條

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

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

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

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

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

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

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

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

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

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

相關博士學位論文 前1條

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

相關碩士學位論文 前10條

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

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

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

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

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

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

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

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

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

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

，

本文編號：2200381