基于Pi演算的服務流驗證方法研究.pdf

1、為了滿足企業(yè)應用系統(tǒng)業(yè)務的快速變化，一種新的軟件系統(tǒng)架構理論-面向服務的架構SOA(Service-Oriented Architecture)應運而生，并引領著軟件行業(yè)新一輪的技術變革。SOA是以服務為基本單位，通過服務重用和快速組合構建隨需應變的松耦合分布式系統(tǒng)，由于單個的Web服務能夠提供的功能有限，為了更加充分地利用共享的Web服務構建企業(yè)級應用系統(tǒng)，Web服務組合技術變得愈加重要。 Web服務組合驗證是在服務組合實際部

2、署前，提前發(fā)現(xiàn)Web服務組合中存在的問題的技術，是Web服務組合走向?qū)嵱玫那疤岷完P鍵。論文結合實驗室承擔的國家支撐計劃、863計劃等國家級重大科研攻關項目，針對驗證服務組合內(nèi)部服務流程邏輯的正確性問題展開研究，探索基于Pi演算的服務流驗證方法，論文主要內(nèi)容如下： 1.基于Pi演算的SFDL模型轉(zhuǎn)換技術。Pi演算作為一種表達能力強大、形式簡潔的形式化方法，特別適合用來描述分布式松耦合的并發(fā)系統(tǒng)。論文首先研究如何用Pi演算建模常見的

3、流程結構模式。然后在分析服務組合描述語言BPEL(Business Process Execution Language)和工作流描述語言XPDL(XML Process Definition Language)的基礎上，提出了服務流程描述語言SFDL(Service Flow Definition Language)，該語言基于XML，易于理解，表達能力強。為實現(xiàn)基于Pi演算的服務流驗證，論文采用基于模式的算法，實現(xiàn)了從SFDL到Pi

4、演算表達式的整體模型轉(zhuǎn)換。 2.基于Pi演算的服務流驗證方法。論文通過Pi演算的操作語義、自動推演等理論來識別和驗證服務流驗證中存在狀態(tài)的可到達性、流程的可完成性等問題。存在上述問題的服務流在轉(zhuǎn)換成Pi演算表達式后都無法順利推演成空進程。本章還分析了利用MWB等工具進行自動化驗證的優(yōu)缺點，針對難以與現(xiàn)有系統(tǒng)集成等問題，論文提出對應的解決方案：在系統(tǒng)中進行Pi演算推演，在推演過程中依次檢查服務流的狀態(tài)可達性、死鎖等問題。