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

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

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

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