服務組合的檢索方法
2023-10-27 06:02:17 3
服務組合的檢索方法
【專利摘要】發明提供一種服務組合的檢索方法，所述方法基於Coq定理證明，Coq是一個基於類型理論的歸納構造證明工具，它具備構造證明和抽取函數式的證明過程的能力，構造證明的過程是自動或者半自動的，服務組合的正確性驗證並不需要在服務組合流程完成後進行檢查，而是由初始的描述和形式證明嚴格保證，從而服務組合的檢索方法比較簡單。
【專利說明】服務組合的檢索方法
【技術領域】
[0001]本發明涉及一種服務組合的檢索方法。
【背景技術】
[0002]隨著計算機和網絡技術的迅速發展，面向服務的計算(service orientedcomputing, S0C)和面向服務的構架(service oriented architecture, SOA)已經成為軟體開發產業的重要技術。SOC和SOA的本質在於以鬆散耦合的分布式為基礎，通過標準信息協議解決大規模資源共享和協調的問題。構建面向服務的系統包含三個主要方面:1.Web服務發現(Discovery)，在提供了可靠服務倉庫的基礎之上，系統應當能夠快速高效的找到滿足服務請求的目標服務；2.Web服務組合(composition)，實際場景中的服務要求往往比較複雜，因此，系統應當提供某些手段來組合原子服務來達到目標；3.組合服務驗證(verification),因此，系統應當能夠證明所提供組合服務的正確性，即其能夠滿足服務要求的能力。
[0003]目前在web服務的研究領域，關於上述方面的技術方法層出不窮，同時越來越到的企業組織傾向於構建跨企業的web服務聚合應用。因此，在運行時高效的選擇和集成易購服務組合服務已經成為學術界和工業界研究者共同關注的熱點。
[0004]事實上，為了簡化集成系統，若干研究成果已經被提出，並且多數已得到領域內研究者們的廣泛認可和實用:UDDI (Universal Description,Discovery and Integration),即通用描述、發現與集成協議，提供基於web服務的註冊和發現機制；WSDL (web ServiceDescription Language),即web服務描述語言，描述web服務的公共接口以實用；S0AP(Simple Object Access Protocol),即簡單對象訪問協議,提供交換數據的協議規範；以及語義web服務描述語言0WL_S(web Ontology Language for Service),旨在為語義網的自動發現、調用和組合服務等提供支持。此外還有描述服務執行的語言規範BPEL/BPEL4WS(Business Process Execution Language for web service)描寫業務過程用於自動執行。
[0005]此外，越來越多的服務組合方式陸續被學者指出，從不同的角度和理論基礎對方法進行闡述和分析，並且有部分方法已經得到實現。有結合工作流的靜態和動態組合方法，有結合Al理論的自動規則方法，有基於依賴關係圖的搜索組合方法，也有基於QoS屬性計算最優化的選擇組合方法等。
[0006]上述已經提出的標準和方法等為組合服務發現和執行提供了基礎的支持，而不同的組合理論和方法也為服務組合提供不同的思路和優化的可能，儘管如此，web服務組合依舊是一個複雜的任務。
[0007]主要原因是:1.可用web服務的數量規模已經超出人類手動分析的能力範圍
2.Web服務通常可以隨時進行發布，更新或刪除等，因此組合服務系統需要在運行時進行檢測並做出反應以保證其可用性3.Web服務通常是由不同的企業組織發布的，在概念模型的使用和表述上各不相同，因此需要相關的語義信息進行分析。此外，服務組合的複雜性還應當包括其自我驗證的複雜性，即上文提到滿足要求服務的正確性。[0008]因此，有必要設計一種簡單的服務組合的檢索方法。
【發明內容】
[0009]針對現有技術存在的缺陷，本發明的目的在於提供一種簡單的服務組合的檢索方法。
[0010]一種服務組合的檢索方法，所述方法基於Coq定理證明。
[0011]優選的，所述檢索方法包括以下步驟:需求輸入、形式轉換、推理證明、抽取結果並最終產生執行過程。
[0012]優選的，所述檢索方法包括以下流程:
[0013]I)採用WSDL文件作為基礎的服務描述；
[0014]2)採用OWL文件擴展服務資源的語意；
[0015]3)把WSDL的operation元素看成一個原子過程；
[0016]4)通過Lemma或Theorem命令聲明用戶希望的給定輸入和輸出服務規則，並且通過流程I)、流程2)、流程3)定義；
[0017]5)通過Coq系統自動證明服務規則；
[0018]6)通過GNU-Flex、GNU-Bison完成服務規則的詞法、語法分析；
[0019]7)通過定義的BNF文法產生對應的LALR分析器，並產生自定向下的構建語法樹；
[0020]8)遍歷語法樹生成服務流程拓撲關係；
[0021]9)將拓撲關係圖轉換成最終的BPEL流程。
[0022]優選的，所述步驟I)中，web服務擁有屬性包括名稱、描述、提供者和參數的輸入、輸出、調入方式和背景若干基礎服務；其中WSDL文件描述這些web服務，並說明他們的屬性。
[0023]優選的，所述步驟2)中，通過OWL文件擴展web服務資源的語義；其中OWL文件中對服務本體的補充定義中，解決了名字不同而予以相同的數據類型的匹配問題。
[0024]優選的,所述步驟3)中，把operation元素看成一個原子過程,貝U其input元素和output元素分別對應輸入I與輸出O,而fault對應了異常信息E,注意到input與output的參數message本身是一個複雜元素,有多個類型的part組成，因此在實際規則定義中，需要將這些part元素通過類型連結符組合表達式為輸入和輸出。
[0025]優選的，所述步驟4)中，對於給定了輸入和期望輸出的用戶需求，同樣可採用I)、
2)、3)、的方法定義為需要求解的目標類型,通過Le_a或Theorem命令來聲明。
[0026]優選的，所述步驟5)中，通過Coq系統證明服務組合，在系統中，Coq產生的組合證明是形如「fun參數列表=> 函數體」的X項，而由於服務數量產生的假設規則增加，使得證明結果中的X項的嵌套層次加深，並且由於其匿名定義的特徵，在函數作用的參數和函數體的定義中也可直接聲明X項並立即調用，因而對X項的聲明需要自頂向下解析並記錄，而對聲明和調用的類型檢查需要自底向上地進行。
[0027]優選的，所述步驟6)中，證明解析的功能實際上相當於一個編譯器前端的功能，通過分析coq證明結果的函數表述構造系統內部服務組合模型，繼而進入後端用於生成執行流程，因此需要對輸出結果進行詞法語法分析，並構造語法書，服務組合引擎通過GNU-Flex、GUN-Bison進行詞法語法分析。[0028]優選的，所述步驟7)中，使用配套的Flex配套工具GNU-Bison，通過我們定義的BNF文法產生對應的LALR分析器，結合我們對每條文法定義的操作行為自底向上的構建語法書。雖然在coq的官方說明中給出了 Gallina文法的完整說明，但是在本系統中使用到的證明方法僅僅是其子集，因此我們對前者進行簡化和重新定義以減少LALR的分析狀態，一定程度上降低了語法分析的複雜度。
[0029]與現有技術相比，本發明至少具有如下技術效果:Coq是一個基於類型理論的歸納構造證明工具，它具備構造證明和抽取函數式的證明過程的能力，構造證明的過程是自動或者半自動的，服務組合的正確性驗證並不需要在服務組合流程完成後進行檢查，而是由初始的描述和形式證明嚴格保證，從而服務組合的檢索方法比較簡單。
【專利附圖】
【附圖說明】
[0030]圖1負載分類方法流程圖。
[0031]圖2WSDL文件及含有相關語義星系定義的OWL文件片段。
[0032]圖3語法樹節點結構實例。
[0033]圖4服務組合拓撲圖。
[0034]圖5圖4服務組合的coq代碼。
[0035]圖6BPEL活動元素。
【具體實施方式】
[0036]在下面的描述中闡述了很多具體細節以便於充分理解本發明。但是本發明能夠以很多不同於在此描述的其它方式來實施，本領域技術人員可以在不違背本發明內涵的情況下做類似推廣，因此本發明不受下面公開的具體實施例的限制。
[0037]參見圖1?圖6，示出本發明一個實施例。服務組合的檢索方法，檢索方法基於Coq定理證明。Coq是一個基於類型理論的歸納構造證明工具，它具備構造證明和抽取函數式的證明過程的能力，構造證明的過程是自動或者半自動的，服務組合的正確性驗證並不需要在服務組合流程完成後進行檢查，而是由初始的描述和形式證明嚴格保證，從而服務組合的檢索方法比較簡單。
[0038]具體的，該檢索方法包括以下步驟:需求輸入、形式轉換、推理證明、抽取結果並最終產生執行過程。
[0039]需求輸入:用戶輸入組合需求。
[0040]形式轉換:即服務規則抽取，將服務和定義好的用戶需求轉換成coq系統的規則和命題描述。其中，採用WSDL文件作為基礎的服務描述，結合OWL文件來擴展服務資源的語義。
[0041]推理證明:自動證明服務組合，coq證明系統，讀入上一模塊的輸出進行自動求解。證明解析模塊的功能實際上相當於一個編譯器前端的功能，通過分析coq證明結果的函數式描述構造系統內部的服務組合模型，繼而進入後端用於生成執行流程，因此如大多數語言的編譯器一樣，需要首先對輸出結果進行詞法分析，定義並構造出抽象語法樹。
[0042]抽取結果:構建完語法樹後，需要對其進行遍歷以生成服務流程的拓撲關係。
[0043]執行過程:在構造完服務流程的拓撲圖之後，可以著手將其轉化成最終的BPEL流程圖。然而BPEL本省的預付是樹形結構，與拓撲關係有著一定區別；並且在拓撲關係中服務節點的信息有限，無法以此直接構造出BPEL流程，需要藉助相應WSDL文件的描述來完成這一件工作。
[0044]本發明中提出的一種服務組合的檢索方法，該方法在保留一定web語義信息的同時增強了組合的靈活性，相較於手動組合方法更加具有更好的效率。
[0045]檢索方法藉助了 MLTT的形式化描述和推理，對本系統來說在邏輯上保證了組合正確性，對MLTT來說擴展了其研究應用範圍。
[0046]設計從證明到BPEL流程轉化的方法具可擴展性，並且可以推過到其他包含類似環節的檢索方法中。
[0047]更具體的，包括以下流程:
[0048]I)採用WSDL文件作為基礎的服務描述；
[0049]2)採用OWL文件擴展服務資源的語意；
[0050]3)把WSDL的operation元素看成一個原子過程；
[0051]4)通過Lemma或Theorem命令聲明用戶希望的給定輸入和輸出服務規則，並且通過流程I)、流程2)、流程3)定義；
[0052]5)通過Coq系統自動證明服務規則；
[0053]6)通過GNU-Flex、GNU-Bison完成服務規則的詞法、語法分析；
[0054]7)通過定義的BNF文法產生對應的LALR分析器，並產生自定向下的構建語法樹；
[0055]8)遍歷語法樹生成服務流程拓撲關係；
[0056]9)將拓撲關係圖轉換成最終的BPEL流程。
[0057]本發明是設計和實現一種基於coq定理證明的服務組合引擎。圖1現實了服務組合引擎的框架圖，包括:
[0058]組合需求:基本的服務組合和用戶定義的服務組合需求。
[0059]語義信息庫:定義並且收集一些基本服務的語義。
[0060]Web服務:描述基本的web服務。
[0061]BPEL流程:將web服務流程拓撲結果生成BPEL流程圖，從而產生可執行的流程。
[0062]規則抽取器:負責將服務和定義好的用戶需求轉換成coq系統的規則和命題描述。
[0063]定理證明機:coq證明系統，讀入上一模塊的輸出進行自動求解。
[0064]轉譯器:首先對coq的證明結果進行解釋，產生服務組合的拓撲關係，然後在此基礎上遍歷生成BPEL的執行流程。
[0065]具體web服務組合引擎的工作流程如下
[0066]第一、用戶在組合需求模塊中輸入用戶服務需求組合。
[0067]第二、通過規則抽取器抽取服務規則，將服務和定義好的用戶需求轉換成coq系統的規則和命題描述。Web服務擁有若干屬性包括服務名稱、描述、提供者和其他參數包括輸入、輸出、調用方式和背景等。在設計中，服務的非功能性屬性沒有考慮在內，原因在於本系統的出發點事立足定理證明，而非專注於組合的Qos優化；其次coq的自動證明策略並不支持證明過程中的複雜計算，需要輔助定義和不封手動證明，這與自動組合殷勤的目的相違背。[0068]對於用來抽象規則的web服務對象，採用WSDL文件作為基礎的服務描述，結合OWL文件來擴展服務資源的語義。圖2展示了一個WSDL文件及含有相關語義信息定義的OWL文件片段。對於WSDL文件,把operation元素看作一個原子過程,則其input元素和output元素分別對應輸出0，而default對應了異常信息E。
[0069]第三、自動證明服務組合，coq證明系統，讀入上一模塊的輸出進行自動求解。證明解析模塊的功能實際上相當於一個編譯器前端的功能，通過分析coq證明結果的函數式描述構造系統內部的服務組合模型，繼而進入後端用於生成執行流程，因此如大多數語言的編譯器一樣，需要首先對輸出結果進行詞法分析，定義並構造出抽象語法樹。本系統通過GNU-Flex和GNU-Flex完成語法詞法分析。其中，語法分析的結果應對一顆語法分析樹，其節點由我們之前定義的記號類通過指針連接，結果如圖3所示。
[0070]第四、生成服務拓撲圖:構建完語法樹後，需要對其進行遍歷以生成服務流程的拓撲關係。圖4和圖5分別顯示了服務組合拓撲圖和該組合在coq系統中的證明代碼。
[0071]第五、模型生成:在構造玩服務流程的拓撲圖之後，可以著手將其轉化成最終的BPEL流程圖。然而BPEL本省的預付是樹形結構，與拓撲關係有著一定區別；並且在拓撲關係中服務節點的信息有限，無法以此直接構造出BPEL流程，需要藉助相應WSDL文件的描述來完成這一件工作。BPEL主要包括定義不封和活動部分:前者包含服務連接和使用變量的定義，其中服務連結描述了一個子服務調用中角色的定義，而變量則類似於WSDL中的message元素，用於定義活動元素中參數的類型以及臨時服務數據的存儲結構；後者分為基本活動和結構性活動。圖6顯示了 BPEL活動元素。
[0072]本發明雖然以較佳實施例公開如上，但其並不是用來限定本發明，任何本領域技術人員在不脫離本發明的精神和範圍內，都可以做出可能的變動和修改，因此本發明的保護範圍應當以本發明權利要求所界定的範圍為準。
【權利要求】
1.一種服務組合的檢索方法，其特徵在於:所述檢索方法基於Coq定理證明。
2.根據權利要求1所述的檢索方法，其特徵在於:所述檢索方法包括以下步驟:需求輸入、形式轉換、推理證明、抽取結果並最終產生執行過程。
3.根據權利要求1所述的服務組合的檢索方法，其特徵在於:所述檢索方法包括以下流程: 1)採用WSDL文件作為基礎的服務描述； 2)採用OWL文件擴展服務資源的語意； 3)把WSDL的operation元素看成一個原子過程； 4)通過Lemma或Theorem命令聲明用戶希望的給定輸入和輸出服務規則，並且通過流程I)、流程2)、流程3)定義； 5)通過Coq系統自動證明服務規則； 6)通過GNU-Flex、GNU-Bison完成服務規則的詞法、語法分析； 7)通過定義的BNF文法產生對應的LALR分析器，並產生自定向下的構建語法樹； 8)遍歷語法樹生成服務流程拓撲關係； 9)將拓撲關係圖轉換成最終的BPEL流程。
4.根據權利要求3所述的服務組合的檢索方法，其特徵在於，所述步驟I)中，web服務擁有屬性包括名稱、描述、提供者和參數的輸入、輸出、調入方式和背景若干基礎服務；其中WSDL文件描述這些web服務，並說明他們的屬性。
5.根據權利要求3所述的服務組合的檢索方法，其特徵在於:所述步驟2)中，通過OWL文件擴展web服務資源的語義；其中OWL文件中對服務本體的補充定義中，解決了名字不同而予以相同的數據類型的匹配問題。
6.根據權利要求3所述的服務組合的檢索方法，其特徵在於:所述步驟3)中，把operation元素看成一個原子過程,則其input元素和output元素分別對應輸入I與輸出O,而fault對應了異常信息E,注意到input與output的參數message本身是一個複雜元素，有多個類型的part組成，因此在實際規則定義中，需要將這些part元素通過類型連結符組合表達式為輸入和輸出。
7.根據權利要求3所述的服務組合的檢索方法，其特徵在於:所述步驟4)中，對於給定了輸入和期望輸出的用戶需求，同樣可採用1)、2)、3)、的方法定義為需要求解的目標類型，通過Lemma或Theorem命令來聲明。
8.根據權利要求3所述的服務組合的檢索方法，其特徵在於:所述步驟5)中，通過Coq系統證明服務組合，在系統中，Coq產生的組合證明是形如「fun參數列表=> 函數體」的X項，而由於服務數量產生的假設規則增加，使得證明結果中的X項的嵌套層次加深，並且由於其匿名定義的特徵，在函數作用的參數和函數體的定義中也可直接聲明X項並立即調用，因而對X項的聲明需要自頂向下解析並記錄，而對聲明和調用的類型檢查需要自底向上地進行。
9.根據權利要求3所述的服務組合的檢索方法，其特徵在於:所述步驟6)中，證明解析的功能實際上相當於一個編譯器前端的功能，通過分析coq證明結果的函數表述構造系統內部服務組合模型，繼而進入後端用於生成執行流程，因此需要對輸出結果進行詞法語法分析，並構造語 法書，服務組合引擎通過GNU-Flex、GUN-Bison進行詞法語法分析。
10.根據權利要求1所述的服務組合的檢索方法，其特徵在於:所述步驟7)中，使用配套的Flex配套工具GNU-Bison，通過我們定義的BNF文法產生對應的LALR分析器，結合我們對每條文法定義的操作行為自底向上的構建語法書。雖然在coq的官方說明中給出了Gallina文法的完整說明，但是在本系統中使用到的證明方法僅僅是其子集，因此我們對前者進行簡化和重新定義`以減少LALR的分析狀態，一定程度上降低了語法分析的複雜度。
【文檔編號】G06F17/30GK103823875SQ201410070573
【公開日】2014年5月28日 申請日期:2014年2月28日 優先權日:2014年2月28日
【發明者】李瑩, 張加省, 尹建偉, 鄧水光, 吳建, 吳朝暉 申請人:浙江大學