面向服務(wù)的業(yè)務(wù)事務(wù)建模與驗(yàn)證方法研究.pdf

1、面向服務(wù)的計算(Service-Oriented Computing，SOC)是一種以Web服務(wù)作為基本組件的分布式計算模式，它支持開放、動態(tài)和異構(gòu)環(huán)境下分布式應(yīng)用的系統(tǒng)集成。Web服務(wù)正從最初關(guān)注描述、發(fā)布和交互向支持健壯的業(yè)務(wù)協(xié)作新階段發(fā)展。為了保證面向服務(wù)的應(yīng)用獲得正確、一致的執(zhí)行結(jié)果，大多數(shù)工作流和B2B協(xié)作應(yīng)用程序都需要支持復(fù)雜的、長時間運(yùn)行的業(yè)務(wù)事務(wù)。面向服務(wù)的業(yè)務(wù)流程除了關(guān)注服務(wù)組合業(yè)務(wù)流程的功能特性外，應(yīng)該整合考慮合成之

2、上的事務(wù)特性。如何設(shè)計正確的Web服務(wù)組合業(yè)務(wù)流程，讓它們協(xié)同工作并保持一致，即確保面向服務(wù)的業(yè)務(wù)事務(wù)(Business Transactions for Services，BTS)正確地執(zhí)行是當(dāng)前一個具有挑戰(zhàn)性的重要問題。
　　本文從操作系統(tǒng)進(jìn)程管理的視角提出了面向服務(wù)的業(yè)務(wù)事務(wù)的概念視圖，將現(xiàn)階段的事務(wù)處理歸結(jié)為在業(yè)務(wù)流程執(zhí)行過程中對服務(wù)、活動及流程的分層管理。從建模語言到驗(yàn)證方法、從建模分析到驗(yàn)證實(shí)現(xiàn)，本文為面向服務(wù)的業(yè)務(wù)事

3、務(wù)的正確性保障建立了一套系統(tǒng)的解決方案。主要研究成果如下:
　　(1)提出了一種支持非功能性描述的移動進(jìn)程代數(shù)MPi-演算。根據(jù)應(yīng)用語義需求引入進(jìn)程作用域的概念，擴(kuò)展了Pi-演算進(jìn)程移動性的含義。用鏈接相對進(jìn)程作用域的移動來表示進(jìn)程的移動，使得MPi-演算能夠描述組件之間交互行為的非功能屬性，具有兼顧系統(tǒng)功能性和非功能性描述的表達(dá)能力。提出了一種膜互模擬關(guān)系，使得在進(jìn)程作用域內(nèi)部具有不同行為的兩個進(jìn)程也可以被認(rèn)為是等價的，并引入了

4、膜等價概念，得出與強(qiáng)/弱互模擬等價類似的性質(zhì)。
　　(2)提出了一種等價自動機(jī)轉(zhuǎn)換的模型驗(yàn)證方法。MPi-演算能夠被解釋成標(biāo)號遷移系統(tǒng)(Labelled Transition System，LTS)，NuSMV是基于Kripke結(jié)構(gòu)(Kripke Structure，KS)的符號模型檢驗(yàn)器，LTS與KS都屬于狀態(tài)自動機(jī)(State Automata)。根據(jù)元模型LTS和KS之間的語義映射關(guān)系，給出了從MPi-演算模型到NuSMV的

5、輸入語言SMV的語法轉(zhuǎn)換規(guī)則?；谠Ｐ投x的語義映射關(guān)系和語法轉(zhuǎn)換規(guī)則可以提高模型轉(zhuǎn)換的可復(fù)用性和可移植性。
　　(3)在服務(wù)層研究了如何保持業(yè)務(wù)流程參與者之間的協(xié)調(diào)一致性問題，提出了支持業(yè)務(wù)事務(wù)驗(yàn)證的服務(wù)協(xié)調(diào)模型。針對Web服務(wù)事務(wù)標(biāo)準(zhǔn)(WS-TX)定義的參與者之間交互消息缺乏嚴(yán)格的語義，用Pi-演算形式化描述了WS-TX規(guī)范中定義業(yè)務(wù)活動事務(wù)的WS-BA協(xié)議，在此基礎(chǔ)上建立了適用于多個參與者的服務(wù)協(xié)調(diào)模型，并驗(yàn)證分析了協(xié)議的

6、安全性和活性。實(shí)驗(yàn)結(jié)果表明，基于服務(wù)協(xié)調(diào)模型的業(yè)務(wù)事務(wù)驗(yàn)證方法，能夠有效地提高業(yè)務(wù)流程執(zhí)行的可靠性和一致性。
　　(4)在活動層研究了如何利用Web服務(wù)事務(wù)模型分析事務(wù)的等價性問題，提出了面向服務(wù)的柔性事務(wù)建模與分析方法。用MPi-演算對柔性事務(wù)模型進(jìn)行了形式化描述，考慮進(jìn)程行為的事務(wù)依賴性，提出了一種事務(wù)膜等價關(guān)系。通過一個典型的柔性事務(wù)實(shí)例，闡述了利用事務(wù)膜開互模擬分析事務(wù)等價關(guān)系的方法。實(shí)驗(yàn)結(jié)果表明，事務(wù)膜開互模擬分析方法能

7、夠判別事務(wù)等價關(guān)系，約簡目標(biāo)系統(tǒng)模型，有效降低系統(tǒng)驗(yàn)證的復(fù)雜度。
　　(5)在流程層研究了如何保證跨組織業(yè)務(wù)流程的可靠性問題，提出了跨組織多業(yè)務(wù)事務(wù)的建模與驗(yàn)證方法。將進(jìn)程的動作交互與跨組織膜活動建立動態(tài)關(guān)聯(lián)，提出了跨組織多業(yè)務(wù)事務(wù)建模方法。驗(yàn)證分析了多業(yè)務(wù)事務(wù)中排他性、響應(yīng)性、非阻塞性和非平凡性等關(guān)鍵性質(zhì)。實(shí)驗(yàn)結(jié)果表明，對于復(fù)雜的多業(yè)務(wù)事務(wù)，經(jīng)過抽象或分解后，同樣能夠采用該方法保障多業(yè)務(wù)流程在設(shè)計與實(shí)現(xiàn)過程中的可靠性。