[發(fā)明專利]一種正確性可保證的自動服務(wù)組合方法及系統(tǒng)

無效

• 申請?zhí)枺?/td>: 200910235612.8
• 申請日: 2009-09-30
• 公開（公告）號: CN101695079A
• 公開（公告）日: 2010-04-14
• 發(fā)明（設(shè)計）人: 懷進鵬;杜宗霞;鄧婷;劉旭東;李翔;孫海龍
• 申請（專利權(quán)）人: 北京航空航天大學(xué)
• 主分類號: H04L29/08
• 分類號: H04L29/08
• 代理公司: 北京同立鈞成知識產(chǎn)權(quán)代理有限公司 11205
• 代理人: 劉芳

1.一種正確性可保證的自動服務(wù)組合方法，其特征在于包括：

獲取安全性規(guī)范、活性規(guī)范和消息映射；

將所述消息映射轉(zhuǎn)化為計算機邏輯公式規(guī)范；

獲取業(yè)務(wù)處理執(zhí)行語言文件；

將所述業(yè)務(wù)處理執(zhí)行語言文件轉(zhuǎn)化為自動機模型文件；

根據(jù)所述自動機模型文件以預(yù)設(shè)算法構(gòu)造滿足所述安全性規(guī)范、所述活性規(guī)范和所述消息映射所轉(zhuǎn)換的計算機邏輯公式規(guī)范的極大組合服務(wù)；

輸出所述極大組合服務(wù)。

2.根據(jù)權(quán)利要求1所述的方法，其特征在于所述根據(jù)所述自動機模型文件以預(yù)設(shè)算法構(gòu)造的滿足所述安全性規(guī)范、所述活性規(guī)范和所述消息映射所轉(zhuǎn)換的計算機邏輯公式規(guī)范的極大組合服務(wù)具體包括：

根據(jù)所述自動機模型文件以預(yù)設(shè)算法構(gòu)造滿足所述安全性規(guī)范和所述消息映射轉(zhuǎn)換的計算機邏輯公式規(guī)范的極大安全組合服務(wù)；

判斷所述極大安全組合服務(wù)是否存在死鎖狀態(tài)，如果存在，則判斷是否可以消除死鎖狀態(tài)，如果可以，則消除死鎖狀態(tài)構(gòu)造無死鎖的極大安全組合服務(wù)；

對所述無死鎖的極大安全組合服務(wù)進行活性驗證，以供通過所述活性驗證后確定所述無死鎖的極大安全組合服務(wù)為極大組合服務(wù)。

3.根據(jù)權(quán)利要求2所述的方法，其特征在于所述根據(jù)所述自動機模型文件以預(yù)設(shè)算法構(gòu)造滿足所述安全性規(guī)范和所述消息映射所轉(zhuǎn)換的計算機邏輯公式規(guī)范的極大安全組合服務(wù)具體包括：

判斷預(yù)設(shè)觀察表(ST，EX，T)是否封閉，如果封閉，則根據(jù)所述觀察表構(gòu)造出自動機C，所述S為服務(wù)集合，表示為S＝{S₁，S₂，...，S_n}；所述S_i為一個自動機，表示為S_i＝(Q_i，∑_i，δ_i，q_i0，F(xiàn)_i，Lab_i)，i＝1，2，...，n；所述∑_i為自動機C的輸入與輸出動作集合，∑_i為自動機C的輸入與輸出動作集合的補動作，∑為組合服務(wù)動作集合，表示為∑＝∑₁∪∑₂∪...∪∑_n；所述ST和所述EX為∑上的字符串，ST＝EX＝{ε}，所述ε表示一個空動作；所述T為(ST∪ST·∑)·EX到{true，false}的函數(shù)，T(σ)＝true，當(dāng)且僅當(dāng)σ∈L_safe，所述L_safe為∑上滿足安全性規(guī)范和消息映射的字符串集合；

判斷子集查詢是否為真，如果為真，則判斷超集查詢是否為真，如果為真，則確定自動機C為極大安全組合服務(wù)C_safe。

4.根據(jù)權(quán)利要求3所述的方法，其特征在于所述判斷子集查詢具體包括：

構(gòu)造服務(wù)集合與自動機的完全交互，所述交互的結(jié)果為并發(fā)組合；

判斷是否完全交互，如果是，則利用模型檢測器對所述并發(fā)組合進行檢測；

通過所述檢測，則判斷子集查詢?yōu)檎妗?/p>

5.根據(jù)權(quán)利要求3所述的方法，其特征在于所述判斷超集查詢具體包括：

構(gòu)造服務(wù)集合與自動機的完全交互，并從自動機的狀態(tài)集合中選擇一個狀態(tài)和所述自動機的一個未定義動作，以供所述服務(wù)集合與所述自動機同步；

根據(jù)所述狀態(tài)和所述未定義動作構(gòu)造交互樹，從所述自動機的狀態(tài)集合中減去所述狀態(tài)；

利用模型檢測器對所述交互樹進行檢測；

未通過所述檢測，則判斷所述自動機的狀態(tài)集合是否為空，如果為空，則判斷超集查詢?yōu)檎妗?/p>

6.根據(jù)權(quán)利要求2所述的方法，其特征在于所述判斷所述極大安全組合服務(wù)是否存在死鎖狀態(tài)，如果存在，則判斷是否可以消除死鎖狀態(tài)，如果可以，則消除死鎖狀態(tài)構(gòu)造無死鎖的極大安全組合服務(wù)具體包括：

構(gòu)造與自動機完全交互的服務(wù)集合，所述交互的結(jié)果為并發(fā)組合；

構(gòu)造所述并發(fā)組合的死鎖狀態(tài)集合；

判斷所構(gòu)造的死鎖狀態(tài)集合是否為非空，如果是，則選擇所述死鎖狀態(tài)集合中的元素，從所述元素向后可達性搜索，并記錄所有可達狀態(tài)；

判斷所述可達狀態(tài)是否包含初始狀態(tài)，如果不是，則從所述并發(fā)組合中去掉所述可達狀態(tài)中所有狀態(tài)和相應(yīng)變遷，并從所述死鎖狀態(tài)集合中去掉所述元素。