Web服務(wù)組合形式化建模與驗(yàn)證研究.pdf

1、面向服務(wù)的體系結(jié)構(gòu)SOA(Service-Oriented Architeture)是一種新的分布式應(yīng)用程序體系結(jié)構(gòu)，它是構(gòu)件重用和分布式技術(shù)發(fā)展的結(jié)果，業(yè)界提出將面向服務(wù)的體系結(jié)構(gòu)作為軟件體系結(jié)構(gòu)下一個發(fā)展階段來幫助IT組織應(yīng)對所面臨的越來越多的復(fù)雜性挑戰(zhàn)。Web服務(wù)(Web Services)是當(dāng)前實(shí)現(xiàn)SOA范型最有前景的技術(shù)。Web服務(wù)技術(shù)的廣泛應(yīng)用使得Web服務(wù)正逐步成為Internet網(wǎng)絡(luò)環(huán)境中資源封裝的標(biāo)準(zhǔn)形式。隨著部署在I

2、nternet上的Web服務(wù)不斷豐富，這些可被公共訪問和集成的服務(wù)構(gòu)成了一個潛在的巨大標(biāo)準(zhǔn)組件庫。在Web服務(wù)互操作技術(shù)的基礎(chǔ)上，提供高層的Web服務(wù)集成手段、實(shí)現(xiàn)Web服務(wù)組合成為Web服務(wù)技術(shù)發(fā)展的自然需求?？偨Y(jié)當(dāng)前的Web服務(wù)組合建模方法，主要分為語法方法、語義方法和形式化方法等。相對于其他服務(wù)組合方法，形式化建模方法有不可替代的重要作用。本論文從理論研究和實(shí)踐結(jié)合兩個方面著手，探索服務(wù)組合的形式化建模和驗(yàn)證技術(shù)。本論文的主要工作

3、如下：
　　 1.建立了Web服務(wù)組合形式化模型，重點(diǎn)研究了用于描述Web服務(wù)交互過程的服務(wù)交互過程模型
　　 Web服務(wù)組合模型FMWSC(Formal Model for Web Service Composition)由兩部分組成：服務(wù)描述模型、以及服務(wù)交互過程模型。服務(wù)描述模型基于Web服務(wù)描述語言WSDL(Web Services Description Language)，用于描述Web服務(wù)組合的靜態(tài)信息；服

4、務(wù)交互過程模型用于描述Web服務(wù)的交互過程。Web服務(wù)交互過程模型能清晰表達(dá)Web服務(wù)組合中各組成部分之間的交互，并可模擬Web服務(wù)的交互過程，分析其動態(tài)性質(zhì)。
　　 2.為了保證服務(wù)交互過程的正確性，給出了服務(wù)交互過程的形式化驗(yàn)證方法服務(wù)交互過程的形式化驗(yàn)正方法將模塊化思想與模型驗(yàn)證技術(shù)相結(jié)合，即在對服務(wù)交互過程進(jìn)行形式化驗(yàn)證時，重點(diǎn)驗(yàn)證服務(wù)基本交互過程。服務(wù)交互全過程的性質(zhì)由這些基本過程的性質(zhì)以及這些基本過程的組合方式所決定

5、。采用這種方法的好處是可以有效地降低系統(tǒng)驗(yàn)證的規(guī)模，并提高驗(yàn)證的效率。驗(yàn)證的基本思路是：首先應(yīng)用IMWSC模型的語義轉(zhuǎn)換函數(shù)，將IMWSC描述轉(zhuǎn)換為通信系統(tǒng)演算CCS表示，然后利用CWB-NC工具提供基于模態(tài)邏輯的檢測機(jī)制對IMWSC模型實(shí)例進(jìn)行驗(yàn)證。
　　 3.應(yīng)用FMWSC建立了車輛維修管理系統(tǒng)模型，并應(yīng)用本文提出的服務(wù)交互過程的驗(yàn)證機(jī)制對該系統(tǒng)的主要屬性和行為一致性進(jìn)行了驗(yàn)證
　　 以一個車輛維修管理系統(tǒng)VRMS(

6、Vehicle Repair Management System)為例，詳細(xì)介紹服務(wù)組合模型FMWSC的實(shí)際應(yīng)用。首先給出組成VRMS系統(tǒng)的服務(wù)組件的靜態(tài)描述，然后應(yīng)用服務(wù)交互過程模型給出了(組成VRMS系統(tǒng)的)服務(wù)間的交互過程描述，并應(yīng)用本文給出的服務(wù)交互過程模型的驗(yàn)證機(jī)制對該系統(tǒng)的主要屬性和行為一致性進(jìn)行了實(shí)際驗(yàn)證。在介紹CCML(Cooperative ComputationModeling Language)語言的基礎(chǔ)上，給出了