[發明專利]一種增強SOA可生存性的降級服務替換驗證方法

有效

• 申請號: 201110457694.8
• 申請日: 2011-12-31
• 公開（公告）號: CN102571789A
• 公開（公告）日: 2012-07-11
• 發明（設計）人: 張亮;楊勇
• 申請（專利權）人: 復旦大學
• 主分類號: H04L29/06
• 分類號: H04L29/06;H04L29/08
• 代理公司: 上海正旦專利代理有限公司 31200
• 代理人: 陸飛;盛志范

1.一種增強SOA可生存性的降級服務替換驗證方法，其特征在于具體步驟為：

步驟一、采用進程代數形式化建模WS-BPEL描述文件所體現的組合服務交互協議

利用進程代數這一形式化工具對服務及其組合環境進行形式化建模，其中，成員服務及組合服務的系統模型表示為服務契約；所述服務契約用以描述服務外部可觀測的消息行為；由于WS-BPEL提供了參與組合的服務集合、服務的調用關系和消息的往來信息，這里采用白盒策略描述WS-BPEL流程形式的替換服務和候選服務以及服務組合和替換的上下文環境；

采用????????????????????????????????????????????????演算描述一個WS-BPEL流程服務即服務契約C，具體語法如下：

這里，表示流程服務的一個接口，表示發送消息操作，即沿接口發出消息；表示接收消息操作，即沿接口接收消息?；表示沒有消息交互的內部操作；

根據服務契約的操作語義規則，表示服務契約執行操作后演化為，表示隱藏操作，?意味著在中的消息操作?變為，即，當多個服務組合成一個服務系統時，某些服務可能僅提供部分接口，并且某些接口及其相關消息操作變成了內部不可觀察的；

步驟二、建立流程決策點，分析WS-BPEL流程形式服務的消息交互行為

在WS-BPEL流程服務交互環境中，區分三類服務契約的決策點：

（1）僅有發送消息操作的決策點；?

（2）僅有接受消息操作的決策點；

（3）同時包括發送消息操作和接受消息操作的決策點；

其中，第三類流程決策點是指同一服務接口的發送消息操作和接受消息操作；

步驟三、建立服務替換正確性準則，定義服務相容性

包括兩大部分：其一，是在所有計算路徑上完成屬性；其二，在部分計算路徑上的“測試成功”；

設一組WS-BPEL流程服務組合，記為系統；系統滿足完成相容屬性，記為，如果下列條件之一成立：

(1)?如果是自包含系統，對于任意以致，；

(2)?如果是開放系統，對于任意以致，存在以致；

步驟四、降級服務替換正確性驗證

包括兩部分：其一,服務子契約以較少的可交換消息集保持了所有計算路徑上的服務相容性；其二,服務契約的測試精化，在部分計算路徑上保持了服務相容性；

一個WS-BPEL流程服務契約是另一服務契約的子契約，記為，如果下列條件成立：

（1）如果是一個決策點即頂層操作是一個選擇，那么也是一個和具有相同類型的決策點；

（2）對于每個接收消息操作以致，存在以致；

（3）對于每個發送消息操作以致,存在,以致；

如果，WS-BPEL流程服務契約是的子契約，那么，對于相同的運行環境，替換后不改變系統原有的完成屬性,即：

如果，那么，?；

在使用子契約實施替換后，一個系統仍保持系統原有的相容性；

然而，由于使用子契約實施的替換是不等價替換，所以，系統的某些服務行為可能會受到影響，這個影響分為兩方面：

第一，如果子契約提供了更多的消息接收能力，并且具有相同的發送消息非決定性選擇，那么，這個替換不影響系統的運行，并且系統將具有更多的服務能力；

第二，如果子契約提供了更多的消息接收能力，但是發送消息的非決定性選擇減少，即發送更少的消息，那么，替換會對系統的全局行為產生兩個方面的影響，即：

（1）?較少的消息交換集合；

（2）較少的可完成計算路徑；

最后，實現增強SOA系統可生存性的降級服務替換；

這里，用保留的服務契約來描述降級服務替換后用戶期望保留的系統功能，記為；其中，是WS-BPEL流程服務系統；依據正確服務替換的要求，實施服務替換后必須滿足?；

令，其中，是WS-BPEL流程服務契約，且,；對于任意，?如果下列條件成立：

(1)?；

(2)?對于每個消息發送操作以致,在?中也存在。