基于過程網(wǎng)絡(luò)的服務(wù)協(xié)同計(jì)算模型研究.pdf

1、面向服務(wù)的體系結(jié)構(gòu)(Service-Oriented Architecture，SOA)是一種新的分布式應(yīng)用程序體系結(jié)構(gòu)，它是構(gòu)件重用技術(shù)和分布式技術(shù)發(fā)展的結(jié)果，業(yè)界提出將面向服務(wù)的體系結(jié)構(gòu)作為軟件體系結(jié)構(gòu)下一個(gè)發(fā)展階段來幫助IT組織應(yīng)對所面臨的越來越多的復(fù)雜性挑戰(zhàn)。在這種體系結(jié)構(gòu)中，所有功能都定義為獨(dú)立的服務(wù)，這些服務(wù)帶有定義明確的可調(diào)用接口，可以以預(yù)先定義的順序調(diào)用這些服務(wù)來組裝業(yè)務(wù)應(yīng)用。服務(wù)是平臺(tái)獨(dú)立的、松散耦合的、具有良好定義功

2、能的、分布在Internet網(wǎng)絡(luò)上的軟件模塊。服務(wù)計(jì)算(Service-Oriented Computing，SOC)是一種新的計(jì)算范型，它使用服務(wù)作為基礎(chǔ)構(gòu)造去支持快速、低成本軟件開發(fā)和簡易組裝等分布式應(yīng)用。總結(jié)當(dāng)前主流的服務(wù)計(jì)算模型，其服務(wù)計(jì)算方法主要分為語法方法、語義方法和形式化方法三類，其中語法方法強(qiáng)調(diào)的是服務(wù)組裝中的工作流過程，語義方法旨在自動(dòng)化服務(wù)組裝全過程，形式化方法側(cè)重于服務(wù)組裝的正確性驗(yàn)證。 本文在對當(dāng)前主流服

3、務(wù)計(jì)算方法進(jìn)行分析比較的基礎(chǔ)上提出了一個(gè)基于過程網(wǎng)絡(luò)的服務(wù)協(xié)同計(jì)算模型CCM。一方面，該模型繼承了語法方法強(qiáng)調(diào)工作流組裝過程的優(yōu)點(diǎn)，采用基于工作流的語法方法來描述和組裝服務(wù)；另一方面，該模型借用了形式化方法在服務(wù)組裝正確性驗(yàn)證方面的優(yōu)勢，采用CCS進(jìn)程代數(shù)提供的形式化驗(yàn)證機(jī)制來驗(yàn)證服務(wù)組裝的正確性。Kahn過程網(wǎng)絡(luò)(KPN)模型是一個(gè)基于數(shù)據(jù)流的計(jì)算模型，用于描述通過數(shù)據(jù)流進(jìn)行通信的一系列協(xié)作過程。KPN的基本屬性，包括并發(fā)性、可調(diào)度性

4、、確定性、層級(jí)性和可實(shí)現(xiàn)性使它成為一個(gè)理想的服務(wù)計(jì)算理論模型，但KPN在非確定性系統(tǒng)建模方面的不足限制了它的實(shí)際應(yīng)用，同時(shí)該模型僅提供了兩個(gè)通信事件和一個(gè)計(jì)算事件，三個(gè)事件不足以描述復(fù)雜的服務(wù)交互。本文針對KPN過程網(wǎng)絡(luò)模型在非確定性事件建模方面以及在服務(wù)交互建模方面的不足，增加了不確定性選擇結(jié)構(gòu)，擴(kuò)充了KPN的三個(gè)基本事件，使之更適合建立復(fù)雜的服務(wù)交互模型。 在給出的CCM服務(wù)協(xié)同計(jì)算模型的基礎(chǔ)上，本文設(shè)計(jì)了CCML服務(wù)協(xié)同計(jì)

5、算建模語言并描述了其操作語義。CCML語言是一種語法層次的服務(wù)組裝描述語言，不僅能夠描述服務(wù)的靜態(tài)信息而且能夠描述服務(wù)之間的動(dòng)態(tài)交互。傳統(tǒng)的語法層次的服務(wù)組裝描述語言只注重服務(wù)功能的語法描述，對于服務(wù)行為的描述卻表現(xiàn)為信息不足，容易導(dǎo)致服務(wù)交互異常的發(fā)生。CCML語言克服了傳統(tǒng)服務(wù)組裝語言的這一缺點(diǎn)，其建模的重點(diǎn)是服務(wù)行為及交互服務(wù)的行為組裝。同時(shí)，CCML語言基于一個(gè)標(biāo)準(zhǔn)的過程模型即KPN數(shù)據(jù)流計(jì)算模型，避免了大多數(shù)服務(wù)組裝語言所具有

6、的復(fù)雜控制流結(jié)構(gòu)，有利于服務(wù)組裝的描述與分析，一定程度上提高了服務(wù)組裝的成功率。采用標(biāo)簽轉(zhuǎn)換系統(tǒng)(Labeled Transition System)和CCS基本語法描述了CCML語言的操作語義。 形式化方法對于驗(yàn)證服務(wù)組裝的正確性是一種有效的方法。許多現(xiàn)有的Web服務(wù)組裝描述語言都是非形式化的或半形式化的，容易出錯(cuò)且不易檢測和驗(yàn)證，也沒有相應(yīng)形式化工具的支持，這使得Web服務(wù)組裝的正確性難以保證。為了保證CCM應(yīng)用系統(tǒng)的組裝正

7、確性，本文提出了CCM應(yīng)用系統(tǒng)模型的一個(gè)形式化驗(yàn)證機(jī)制。首先將CCM服務(wù)組裝應(yīng)用系統(tǒng)的CCML描述轉(zhuǎn)換為CCS進(jìn)程代數(shù)描述，然后利用CWB-NC(Concurrency Workbench of the New Century)提供的基于時(shí)序邏輯的檢測機(jī)制和驗(yàn)證工具對CCM應(yīng)用系統(tǒng)模型進(jìn)行屬性驗(yàn)證和服務(wù)兼容性驗(yàn)證。CCS進(jìn)程代數(shù)提供了較高的表達(dá)力，它有足夠的能力來完成CCM應(yīng)用系統(tǒng)模型所需的驗(yàn)證功能。實(shí)踐表明，本文給出的CCM應(yīng)用系統(tǒng)模

8、型的形式化驗(yàn)證機(jī)制是有效的。 本文描述了CCM協(xié)同計(jì)算模型支持環(huán)境的體系結(jié)構(gòu)，采用Java語言實(shí)現(xiàn)了基于KPN的服務(wù)協(xié)同編排器的原型系統(tǒng)，采用Java RMI和Java多線程技術(shù)實(shí)現(xiàn)了服務(wù)交互APIs。 最后，本文詳細(xì)介紹了CCM模型的一個(gè)應(yīng)用系統(tǒng)實(shí)例。采用CCML語言描述了該系統(tǒng)的業(yè)務(wù)流程和服務(wù)之間的動(dòng)態(tài)交互，并采用本文提出的CCM應(yīng)用系統(tǒng)模型的屬性和服務(wù)兼容性驗(yàn)證機(jī)制對該系統(tǒng)的主要屬性和某些交互服務(wù)的兼容性進(jìn)行了實(shí)際