Semantic Web Services的自動(dòng)化組合技術(shù).pdf

1、本論文以Semantic Web Services(語義Web服務(wù))的自動(dòng)化組合技術(shù)為研究的中心，圍繞這一主要問題，分3個(gè)部分分別分析與探討了服務(wù)的語義、組合服務(wù)、以及自動(dòng)化服務(wù)組合的方法。 本論文所有的研究，都是基于服務(wù)的語義進(jìn)行的?！罢Z義”是Semantic Web Services體系中最重要的一個(gè)部分。服務(wù)被解釋成一種特殊的軟件組件，提取其輸入?yún)?shù)((_I)nput)、輸出參數(shù)((_O)utput)、前置條件((_P)r

2、econdition)、執(zhí)行效果((_E)ffect)、以及執(zhí)行功能(IO-（_V）inculum)這5個(gè)要素，即(I，O，P，E，V)，給出了服務(wù)作為一個(gè)整體的語義定義。以此語義定義為基礎(chǔ)，分析了服務(wù)語義之間的關(guān)聯(lián)關(guān)系，給出了“服務(wù)語義匹配”的嚴(yán)格的形式化定義。 對(duì)服務(wù)組合演算的產(chǎn)物—組合服務(wù)，做了深入的分析。組合服務(wù)是一種服務(wù)執(zhí)行流程，以π-Calculus為形式化描述工具，分別以數(shù)據(jù)流模型(DFM)和中心控制點(diǎn)模型(CCM

3、)為視點(diǎn)，定義了兩種表達(dá)形式。定義了基于DFM表述形式的組合服務(wù)語義積分算法(SCA)，用于從組件服務(wù)的語義以及組合模型來獲取組合服務(wù)的語義，這是服務(wù)驗(yàn)證的基礎(chǔ)。定義了基于CCM表述形式的BPEL腳本生成規(guī)則(CCM2BPEL)，用于獲取可發(fā)布執(zhí)行的組合服務(wù)最終形式。給出了從DFM模型到CCM模型的映射算法(DFM2CCM)。 以“證明與程序的等價(jià)理論(Proofas Programs)”為依據(jù)，以“基于推理的程序生成技術(shù)(De

4、ductive Program Synthesis)”為原型，給出了實(shí)現(xiàn)自動(dòng)化服務(wù)組合的技術(shù)解決方案—基于邏輯定理證明的自動(dòng)化服務(wù)組合技術(shù)。依照一個(gè)邏輯公式轉(zhuǎn)換模板，把服務(wù)的語義(I，O，P，E，V)映射成一個(gè)一階謂詞邏輯(First-Order Logic，F(xiàn)OL)定理，以已有服務(wù)作為已知定理，目標(biāo)服務(wù)作為待證明定理。從OWL本體庫以及背景知識(shí)庫中導(dǎo)入相關(guān)的外部語義知識(shí)，以彌合已知定理之間的語義縫隙。應(yīng)用自動(dòng)化定理證明引擎(Autom

5、atic Theorem Prover,ATP)，獲取證明結(jié)果，提取證明路徑。最后利用CSEA算法，從證明路徑中提取目標(biāo)服務(wù)的實(shí)現(xiàn)體(基于DFM模型)，從而構(gòu)建了完整的從需求到最終結(jié)果的技術(shù)路徑(Problem→Proof→DFM→CCM→BPEL)。這種“從證明到程序”的方法，保證了所得組合結(jié)果的完備性與正確性。 通過一個(gè)完整的應(yīng)用示例，對(duì)論文中的各個(gè)關(guān)鍵步驟進(jìn)行了具體的說明與演示。實(shí)現(xiàn)了一個(gè)原型系統(tǒng)，用于對(duì)整套方法進(jìn)行初步的