THP事務(wù)協(xié)調(diào)協(xié)議的形式化分析與驗證.pdf

1、Web服務(wù)是解決分布式結(jié)構(gòu)異構(gòu)性的計算模型，Web服務(wù)中的事務(wù)處理是保證服務(wù)結(jié)果一致性和可靠性的有效技術(shù)。由于Web服務(wù)自身的分布性、異構(gòu)性、自描述等特點(diǎn)，Web服務(wù)中的事務(wù)處理也具有長周期、自治性等特點(diǎn)，傳統(tǒng)的事務(wù)處理技術(shù)不再適應(yīng)。為解決些問題，工業(yè)界提出新的事務(wù)處理協(xié)議，如BTP、WS-C/Tx、WS-CAF、THP等協(xié)議。學(xué)術(shù)上，形式化方法已被用于對基于消息通訊的并發(fā)系統(tǒng)的建模和分析，模型檢測方法在協(xié)議分析上有著抽象、高效等特點(diǎn)。

2、因此將形式化方法用于Web服務(wù)領(lǐng)域已經(jīng)成為一個重要的研究方向。
　　 本文采用形式化方法對支持事務(wù)協(xié)調(diào)的THP協(xié)議進(jìn)行建模與驗證分析。從“結(jié)構(gòu)組件活性驗證”與“業(yè)務(wù)邏輯安全性驗證”兩部分對THP協(xié)議進(jìn)行建模和分析。
　　 針對THP協(xié)議的并發(fā)特性，采用Pi-演算進(jìn)行建模，給出THP協(xié)議結(jié)構(gòu)組件到Pi演算語法的映射表和建模規(guī)則。在對THP協(xié)議各個模塊建模的基礎(chǔ)上，得到THP協(xié)議結(jié)構(gòu)組件的Pi-演算模型，然后運(yùn)用Pi-演算模

3、型檢測工具M(jìn)WB對THP協(xié)議結(jié)構(gòu)組件的死鎖性進(jìn)行檢測，從而驗證了在并發(fā)情況下，THP協(xié)議各結(jié)構(gòu)組件不會產(chǎn)生死鎖。
　　 另一方面，對THP協(xié)議的業(yè)務(wù)邏輯進(jìn)一步驗證。本文給出Schema中消息到Pi-演算的映射規(guī)則，以及THP協(xié)議中WSDL描述到Pi-演算的編碼規(guī)則，從元模型層實現(xiàn)了THP協(xié)議規(guī)范到Pi-演算的映射方法，為THP協(xié)議業(yè)務(wù)邏輯實例的Pi-演算建模提供了分析的基礎(chǔ)。由于MWB不支持時間算子和相關(guān)的邏輯性質(zhì)規(guī)約的推演，本