一種分布式事務通信有限狀態機模型及其驗證方法
2023-09-22 13:43:15 1
專利名稱：一種分布式事務通信有限狀態機模型及其驗證方法
技術領域：
本發明涉及分布式事務環境下，事務協議的有限狀態機模型描述及其驗證方法。
背景技術：
通信有限狀態機(CFSM)是形式化描述和驗證協議的有力工具，具有直觀、易懂、 描述能力強的特點，可有效提高通信協議的嚴謹性和完整性。但當描述對象為分布式事務協議時，傳統的CFSM本身有以下兩點不足(1)傳統CFSM著眼於描述和驗證各狀態機之間通信邏輯上的正確性，而無法應對實際中可能發生的各種異常(如消息延遲、丟失，通信中斷等)。(2)要求終態一致性的事務協議不同於普通的通信協議，它更關注於一次事務能否在有限時間內完成並達到某種一致性的狀態，這是傳統CFSM無法實現的。由於事務協議的特殊性，必須考慮在通信失效等情況下協議可能出現的異常，並且要求事務可以在有限時間內完成和達到終態一致性，這使得CFSM在分布式事務環境下無法較好的應用。
發明內容
本發明的技術解決問題克服現有技術的不足，通過擴展CFSM模型，提出了一種分布式事務通信有限狀態機模型，它通過增加終態集、匹配終態集以及內部事件等方式提高模型的描述力，可以較好的描述分布式事務協議；同時提供了該模型的驗證方法，可以驗證協議的死鎖、死環、可達性、轉移函數冗餘、完整性以及終態一致性六種性質。本發明的技術解決方案一種分布式事務通信有限狀態機模型，其特徵在於分布式事務通信有限狀態機模型可以用一個七元組表示如下 S^i",〈οΑΛ ijJ = Λ〈ΙΑΛ Γ，1n, Ρ> ；其中KSA111為η個分立的有限狀態集，Si代表進程i的狀態集，Oi是Si的一個元素，代表進程i的初態XMijM =廣為η2個分立的有限狀態集，對於任意LMii為空集，而Mij 代表可從進程i發送到進程j的消息KIP111是η個分立的有限狀態集，Ii代表進程i的內部事件；Γ =SiX Σ- (Si5Mij)是狀態轉移函數映射，其中Σ = {m} U {ξ},πι e KMij^, J = 廣}，ξ e Ii,即Σ是一個集合，它包含了狀態機的全部收到/發出一條消息的外部事件和內部事件，若事件σ εΣ，狀態s e Si,則轉移函數Γ (s，σ )表示狀態機在發生事件σ後由狀態s轉移到下一個狀態，1n為η個分立的有限狀態集，Fi代表進程i的終態集；P = Kf1, f2... fn>}，其中& e Fi, P代表η個狀態機滿足一致性的相匹配的終態的集合；根據本發明的一種分布式事務通信有限狀態機模型的驗證方法，其特徵在於步驟如下(1)分布式事務通信有限狀態機模型可以用一個七元組表示如下 S^i",〈οΑΛ KM1^u j = 1n,〈ΙΑΛ Γ，1n, Ρ>(2)分布式事務協議有限狀態機驗證方法是從分布式事務通信有限狀態機 (TCFSM)的初態開始，採用深度優先的方法，生成每個節點的所有可能後繼結點，從而描述一個協議所有進程的所有可能的執行過程。其結果是生成一棵協議樹，該協議樹從根節點到任意葉節點的一條路徑代表該協議從開始到結束的一種可能執行過程。根據本發明的又一個方面，其中步驟(1)進一步包括步驟(la) (SiY為η個分立的有限狀態集，Si代表進程i的狀態集，Oi是Si的一個元素，代表進程i的初態；=廣為η2個分立的有限狀態集，對於任意i，Mii為空集，而Mij 代表可從進程i發送到進程j的消息KIP111是η個分立的有限狀態集，Ii代表進程i的內部事件；Γ =SiX Σ- (Si5Mij)是狀態轉移函數映射，其中Σ = {m} U {ξ},πι e KMij^, J = 廣}，ξ e Ii,即Σ是一個集合，它包含了狀態機的全部收到/發出一條消息的外部事件和內部事件。若事件σ εΣ，狀態s e Si,則轉移函數Γ (s，(O表示狀態機在發生事件ο後由狀態s轉移到下一個狀態。(Fi^n為η個分立的有限狀態集，Fi代表進程i的終態集；P =Kf1, f2. · · fn>}，& e Fi, P代表η個狀態機滿足一致性的相匹配的終態的集合。(Ib)採用二元組來描述全局狀態。S代表η元狀態組Sl，s2. ..Sn，其中Si 代表進程i的當前狀態，Si e Si, C表示η2元組(cn，. . . cln, C21，. . . cj，其中Cij是Mij集元素組成的消息序列，表示從進程i到進程j的信道中包含的消息。此處對任意i，Cii均為空，因為Mii是空集。根據本發明的又一個方面，其中步驟( 進一步包括步驟(2a)初始化初始全局狀態pO (, )，pO是協議樹的根節點，代表協議的初始狀態。Qb)對於節點 p，查找全部狀態 ql，q2，. . . qn，滿足 ρ+σ — qi，σ e { U Σ i}, 選擇一個未被生成的狀態qi，初始化該節點並使其成為P的子節點。循環初始化其後繼節點，直到最後的節點不再有後繼結點(即該節點為葉節點)。回溯到該節點，再另選一個未被生成的狀態qj，重複以上過程，直至整棵樹生成。(2c)驗證死鎖在生成一個節點的所有子節點的過程中，若該節點既不是終結節點，又沒有由內部事件引起狀態轉移生成的子節點，則該節點可能因為消息丟失而發生死鎖；若在此情況下也沒有由外部消息引起的狀態轉移，則該狀態必定發生死鎖。(2d)驗證死環若生成的協議樹深度有限並且所有的葉節點均為終結節點，則該協議無死環。(2e)驗證可達性對有限狀態機的狀態進行標記，若在生成樹的過程中到達過該節點，則該節點標識為「1」。生成結束後若存在不為1的狀態，則該狀態不可達。(2f)驗證轉移函數冗餘對有限狀態機的狀態轉移函數進行標記，若在生成樹的過程中用到過該轉移函數，則該轉移函數標識為「1」。生成結束後若存在不為1的轉移函數，則該轉移函數冗餘。(2g)驗證完整性在建立生成樹的過程中，若信道中的外部消息不能使該節點發生狀態轉移(即沒有匹配的轉移函數)，則說明該消息未被定義，因而不滿足完整性。(2h)驗證終態一致性若生成樹的所有葉節點均為終結節點，並且葉節點的各進程狀態匹配(即 e P)，則滿足終態一致性。本發明與現有技術相比的優點在於本發明可以描述在實際應用中可能出現的各種異常和協議各進程的終態一致性要求，並且可以驗證在此情況下協議的死鎖、死環、終態一致性......等六種性質。
圖1為AUDR總控消息和內部事件定義。圖2為AUDR總控狀態轉移函數定義。圖3為AUDR底層消息和內部事件定義。圖4為AUDR底層狀態轉移函數定義。圖5為AUDR總控有限狀態圖。圖6為AUDR底層有限狀態圖。
具體實施例方式
下面參考附圖，對本發明的實施例進行詳細的說明。首先以具體的事務協議實例——AUDR系統中的事務協議對本發明的TCFSM模型進行說明。非結構化數據管理系統(AdvancedUnstructured Data R印ository，簡稱 AUDR) 是一種集成了文本、圖像、音頻和視頻等非結構化數據管理功能的管理系統。AUDR系統中的事務操作涉及兩個角色，一個是總控伺服器，簡稱「總控」，一個是圖像、音頻等媒體伺服器， 簡稱「底層」。按照模型定義，AUDR事務協議用如下七元組描述 S^/, Λ ijJ = 12,〈ΙΑ2，Γ，12, Ρ>S」 &為2個分立的有限狀態集，分別代表總控與底層的有限狀態集，其中S1 = Unit，updating, waitl，wait2，abort, commit}，代表總控初始化、更新、一階段等待、二階段等待、夭折禾口提交六禾中狀態，S2 = {init, updating, waitcommit, abort, commit, error}, 代表底層初始化、更新、等待提交、夭折、提交和異常六種狀態；0l = init、O2 = init分別代表總控和底層的的初態；M12、M21為2個分立的有限狀態集，其中M12代表從總控發送到底層的消息，M21代表從底層發送到總控的消息，其傳遞對應著有限狀態機的外部事件；Ip I2 對應總控和底層的內部事件集；(總控和底層的消息和內部事件定義見附圖1和附圖3) Γ 是狀態轉移函數映射，其定義見附圖2和附圖4 ；F1,F2為2個分立的有限狀態集，分別代表總控和底層的終態的集合,其中 F1 = {commit, abort}，F2 = {commit, abort, error} ；P = {<commit, commit), , , },代表滿足一致性的相匹配的終態集合。採用二元組代表這樣一個全局狀態總控處於waitl狀態，底層處於init狀態，前者到後者的信道中存在CRE事件。由前述可以得出AUDR總控和底層的狀態機，如附圖5和附圖6所示。其中符號 「_」表示發出消息，符號「 + 」表示接收消息，內部事件則不加標註，用「/」分隔引起狀態轉移的事件和發出的消息。終態用下劃線標明。由此可以看出本發明可以描述在實際應用中可能出現的各種異常和協議各進程的終態一致性要求。本發明的一種分布式事務通信有限狀態機模型的驗證方法如下 (1)初始化初始全局狀態p0 (, )，p0是協議樹的根節點，代表協議的初始狀態。(2)對於節點？，查找全部狀態91，92，...911，滿足？+0 - qi, σ e {UEi}，選擇一個未被生成的狀態qi，初始化該節點並使其成為P的子節點。循環初始化其後繼節點， 直到最後的節點不再有後繼結點(即該節點為葉節點)。回溯到該節點，再另選一個未被生成的狀態qj，重複以上過程，直至整棵樹生成。(3)驗證死鎖在生成一個節點的所有子節點的過程中，若該節點既不是終結節點，又沒有由內部事件引起狀態轉移生成的子節點，則該節點可能因為消息丟失而發生死鎖；若在此情況下也沒有由外部消息引起的狀態轉移，則該狀態必定發生死鎖。(4)驗證死環若生成的協議樹深度有限並且所有的葉節點均為終結節點，則該協議無死環。(5)驗證可達性對有限狀態機的狀態進行標記，若在生成樹的過程中到達過該節點，則該節點標識為「1」。生成結束後若存在不為1的狀態，則該狀態不可達。(6)驗證轉移函數冗餘對有限狀態機的狀態轉移函數進行標記，若在生成樹的過程中用到過該轉移函數，則該轉移函數標識為「1」。生成結束後若存在不為1的轉移函數，則該轉移函數冗餘。(7)驗證完整性在建立生成樹的過程中，若信道中的外部消息不能使該節點發生狀態轉移(即沒有匹配的轉移函數)，則說明該消息未被定義，因而不滿足完整性。(8)驗證終態一致性若生成樹的所有葉節點均為終結節點，並且葉節點的各進程狀態匹配(即 e P)，則滿足終態一致性。應用本發明的AUDR事務協議已在AUDR系統事務協議的設計和驗證上得到了應用，證明了實際的應用效果。對於本領域的普通技術人員來說可顯而易見的得出其他優點和修改。因此，具有更廣方面的本發明並不局限於這裡所示出的並且所描述的具體說明及示例性實施例。因此，在不脫離由隨後權利要求及其等價體所定義的一般發明構思的精神和範圍的情況下， 可對其作出各種修改。
權利要求
1.一種分布式事務通信有限狀態機模型的驗證方法，其特徵在於步驟如下(1)分布式事務通信有限狀態機模型可以用一個七元組表示如下 S^i",〈οΑΛ KM1^u j = 1n,〈ΙΑΛ Γ，1n, Ρ> ；其中KSP111為η個分立的有限狀態集，Si代表進程i的狀態集，Oi是Si的一個元素，代表進程i的初態；〈Μ。、,」=廣為η2個分立的有限狀態集，對於任意LMii為空集，而Mij代表可從進程i發送到進程j的消息KIA111是η個分立的有限狀態集，Ii代表進程i的內部事件；Γ =SiX Σ — (Si, Mij)是狀態轉移函數映射，其中Σ = {m} U {ξ},πι e {〈Μ。、,」=廣}， ξ e Ii,即Σ是一個集合，它包含了狀態機的全部收到/發出一條消息的外部事件和內部事件，若事件σ εΣ，狀態s e Si,則轉移函數Γ (s，σ)表示狀態機在發生事件σ後由狀態s轉移到下一個狀態，1n為η個分立的有限狀態集，Fi代表進程i的終態集；P = Kf1, U .. fn>}，其中& e Fi, P代表η個狀態機滿足一致性的相匹配的終態的集合；(2)分布式事務協議有限狀態機模型的驗證方法是從分布式事務通信有限狀態機 TCFSM的初態開始，採用深度優先的方法，生成每個節點的所有可能後繼結點，從而描述一個協議所有進程的所有可能的執行過程，其結果是生成一棵協議樹，該協議樹從根節點到任意葉節點的一條路徑代表該協議從開始到結束的一種可能執行過程。
2.根據權利要求1所述的分布式事務通信有限狀態機模型的驗證方法，其中步驟(1) 進一步包括步驟採用二元組<S，O來描述全局狀態，S代表η元狀態組Sl，S2. . . \，其中Si代表進程i 的當前狀態，Si e Si, C表示η2元組(cn，. . . cln, C21，...cj，其中Cij是Mij集元素組成的消息序列，表示從進程i到進程j的信道中包含的消息，此處對任意i，Cii均為空，因為Mii 是空集。
3.根據權利要求1所述的分布式事務通信有限狀態機模型的驗證方法，其中步驟(2) 進一步包括步驟(2a)初始化初始全局狀態，pO (, )，pO是協議樹的根節點，代表協議的初始狀態；Ob)對於節點p，查找全部狀態ql，q2，...qn，滿足ρ+σ — qi，σ e {UEi}，選擇一個未被生成的狀態qi，初始化該節點並使其成為P的子節點；循環初始化其後繼節點，直到最後的節點不再有後繼結點，即該節點為葉節點，回溯到該節點，再另選一個未被生成的狀態qj，重複以上過程，直至整棵樹生成；(2c)驗證死鎖在生成一個節點的所有子節點的過程中，若該節點既不是終結節點， 又沒有由內部事件引起狀態轉移生成的子節點，則該節點可能因為消息丟失而發生死鎖； 若在此情況下也沒有由外部消息引起的狀態轉移，則該狀態必定發生死鎖；(2d)驗證死環若生成的協議樹深度有限並且所有的葉節點均為終結節點，則該協議無死環；(2e)驗證可達性對有限狀態機的狀態進行標記，若在生成樹的過程中到達過該節點，則該節點標識為「1」；生成結束後若存在不為1的狀態，則該狀態不可達；(2f)驗證轉移函數冗餘對有限狀態機的狀態轉移函數進行標記，若在生成樹的過程中用到過該轉移函數，則該轉移函數標識為「1」，生成結束後若存在不為1的轉移函數，則該轉移函數冗餘；(2g)驗證完整性在建立生成樹的過程中，若信道中的外部消息不能使該節點發生狀態轉移，即沒有匹配的轉移函數，則說明該消息未被定義，因而不滿足完整性；(2h)驗證終態一致性若生成樹的所有葉節點均為終結節點，並且葉節點的各進程狀態匹配，即 e P，則滿足終態一致性。
4. 一種分布式事務通信有限狀態機模型，其特徵在於分布式事務通信有限狀態機模型可以用一個七元組表示如下 S^i",〈οΑΛ KM1^u j = 1n,〈ΙΑΛ Γ，1n, Ρ> ；其中KSP111為η個分立的有限狀態集，Si代表進程i的狀態集，Oi是Si的一個元素，代表進程i的初態；〈Μ。、,」=廣為η2個分立的有限狀態集，對於任意LMii為空集，而Mij代表可從進程i發送到進程j的消息KIA111是η個分立的有限狀態集，Ii代表進程i的內部事件；Γ =SiX Σ — (Si, Mij)是狀態轉移函數映射，其中Σ = {m} U {ξ},πι e {〈Μ。、,」=廣}， ξ e Ii,即Σ是一個集合，它包含了狀態機的全部收到/發出一條消息的外部事件和內部事件，若事件σ εΣ，狀態s e Si,則轉移函數Γ (s，σ)表示狀態機在發生事件σ後由狀態s轉移到下一個狀態，1n為η個分立的有限狀態集，Fi代表進程i的終態集；P = Kf1, U .. fn>}，其中& e Fi, P代表η個狀態機滿足一致性的相匹配的終態的集合。
全文摘要
一種分布式事務通信有限狀態機模型及其驗證方法(1)分布式事務通信有限狀態機模型可以用一個七元組表示；(2)分布式事務協議有限狀態機驗證方法是從TCFSM的初態開始，採用深度優先的方法，生成每個節點的所有可能後繼結點，從而描述一個協議所有進程的所有可能的執行過程。本發明提出的分布式事務通信有限狀態機模型通過增加終態集、匹配終態集以及內部事件等方式提高模型的描述力，可以較好的描述分布式事務協議；同時提供了該模型的驗證方法。
文檔編號H04L12/24GK102291436SQ20111020733
公開日2011年12月21日 申請日期2011年7月22日 優先權日2011年7月22日
發明者李未, 李航宇, 郎波, 鄭劍 申請人:北京航空航天大學