[發明專利]一種基于SoaML的云應用正確性驗證方法

有效

• 申請號: 201310226221.6
• 申請日: 2013-06-07
• 公開（公告）號: CN103281329A
• 公開（公告）日: 2013-09-04
• 發明（設計）人: 李必信;耿國清;王璐璐;陶傳奇;蘭陽陽;司靜文
• 申請（專利權）人: 東南大學
• 主分類號: H04L29/06
• 分類號: H04L29/06;H04L29/08
• 代理公司: 南京瑞弘專利商標事務所(普通合伙) 32249
• 代理人: 楊曉玲

1.一種基于SoaML的云應用正確性驗證方法，其特征在于，該方法包括如下步驟：

步驟1）建立給定的ServiceInterface元模型到PROMELA元模型的同態映射；

步驟2）將給定的ServiceInterface狀態機采用層次自動機來描述，即以一個四元組SM＝＜＜S,H＞,E,T,D＞來表示ServiceInterface狀態機，其中＜S,H＞表示一個狀態層次，S為有限狀態集合，H為子狀態關系，E為有限狀態集合，T為有限轉換集合，D為缺省狀態集合；

步驟3）定義ServiceInterface狀態機的活動狀態配置C∈2^S和事件隊列Q，所述活動狀態配置C為某一時刻ServiceInterface狀態機所有活動狀態的集合，所述事件隊列Q為觸發事件的隊列；

步驟4）定義一個對偶<C,Q>，用以表示ServiceInterface狀態機的活動狀態配置C與事件隊列Q的格局；

步驟5）定義對偶<C,Q>轉換的約束，

(1)若substates(s)≠Φ，則kind(s)∈{composite,orthogonal};

(2)若kind(s)＝orthogonal，則#substates(s)≥2，并且對于所有s的后繼節點s′，

都有kind(s′)＝composite;

(3)若kind(s)＝composite，則#{s∈substates(s)|kind(s′)＝initial}≤1。

(4)kind(source(t))≠final

(5)kind(target(t))≠initial

(6)若kind(source(t)){initial,fork,join}，則guard(t)＝true;

(7)若kind(source(t))＝initial，則target(t)是非偽狀態(non-pseudostate);

(8)若kind(source(t))＝initial，則container(target(t))＝container(source(t));

(9)若kind(source(t))＝initial，則effect(t)＝skip;

(10)若kind(source(t))＝fork，則target(t)是偽狀態;

(11)若kind(target(t))＝join，則guard(t)＝true;

步驟6）根據所述步驟5）中定義的約束，得到對偶<C，Q>轉換的集合記為FT，具體過程如下：遍歷有限轉換集合T，對每個轉換t進行以下處理：

a）如果轉換t∈FT，則enabled(t,e,C)＝true,并進入步驟d），否則進入條件b)，

b）如果t1,t2∈FT，且t1≠t2，則t1||t2,并進入步驟d），否則進入條件c)，

c）如果t′∈T/FT,t∈FT且enabled(t′,e,C)＝true，則清除FT中的t||t′和t⊥t′后進入步驟d），否則直接進入步驟d）；

d）將該轉換t加入到返回的結果中；

其中FT初始化為＜false,Φ＞，函數enabled(t,e,C)判斷ServiceInterface狀態機格局的轉換是否是使能的；有限轉換集合T中所有的轉換t進行完以上處理后，最終得到的返回的結果即為對偶<C，Q>轉換的集合FT；

步驟7）根據所述步驟1）中建立的SoaML元模型到PROMELA元模型的同態映射，將四元組SM＝＜＜S,H＞,E,T,D＞中的事件、類、狀態、轉換以及對偶<C，Q>轉換的過程采用PROMELA語言表示，作為簡單進程元語言解釋器SPIN的輸入代碼；

步驟8）根據給定的ServiceContract消息編號，寫出線性時序邏輯公式，作為輸入簡單進程元語言解釋器SPIN的代碼；

步驟9）將步驟7）和步驟8）得到的代碼輸入簡單進程元語言解釋器SPIN進行驗證，如兩個代碼一致，則判定云應用正確，否則，判定云應用不正確。

2.根據權利要求1所述的基于SoaML的云應用正確性驗證方法，其特征在于，所述步驟2）中層次自動機的語法按照以下方法定義：

定義Exp為包含true、false、e1^e2布爾表達式的表達式集，Act是由skip語句、串行語句、并行語句組成的動作集，Evt表示完成事件的所有事件集；

建立函數kind，對于給定的ServiceInterface狀態機，kind表示判斷狀態機中的每個狀態s的類型；

ServiceInterface狀態機上的轉換表示為一個五元組t＝＜s,e,g,a,S′＞，其中：s是狀態轉換的源狀態，e是轉換的觸發事件，g是轉換的警戒條件，a是轉換觸發的動作，S′是轉換的目標狀態集；

定義以下五個與轉換有關的函數source(t)＝s表示t的源狀態，trigger(t)＝e轉換t的觸發事件，guard(t)＝g轉換t的警戒條件，effect(t)＝a轉換t引發的效果，target(t)＝s'轉換t的目標狀態；

將唯一的根狀態記為root，root∈S；

建立container()函數和substates()函數來表示狀態之間的父子關系，container()函數的功能為返回狀態集中每一個狀態的父狀態，substates()函數的功能為返回每個狀態的后繼狀態；

建立函數outgoings(s)＝{t∈T|source(t)＝s}，表示狀態s的發出轉換的集合，建立函數incomings(s)＝{t∈T|target(t)＝s}，表示進入狀態s的轉換的集合；

定義source(M)＝{source(t)|t∈M}，target(M)＝{target(t)|t∈M}，其中，表示集合outgoings(s)或者incomings(s)的源狀態集和目標狀態集。