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

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

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

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

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

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

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