UML狀態圖的檢測算法生成

王佳婧++馮長寶++佟鑫

摘 要在軟件系統設計中，經常應用UML 狀態圖對系統行為進行完整建模，其正確性尤為重要。在其他文獻中雖然已提出基于HA和EMC的檢測規則，但是并未給出具體算法。因此根據算法生成的關鍵問題主要探討：基于狀態圖HA的自動生成及存儲、基于HA的Kripke自動生成、以及基于Kripke結構和EMC檢測規則的算法實現。

【關鍵詞】HA自動生成 Kripke自動生成 檢測規則算法實現

1 引言

UML狀態圖檢測采用HA的Kripke結構表示，使多對象組成的復雜軟件系統的行為狀態層次清晰，使對象內狀態轉換與整個系統的狀態轉換之間關系表達更加直觀。在其他文獻中已經提出了基于此種結構及EMC思想的檢測規則。其算法生成的關鍵問題如下：狀態圖如何自動轉換為HA；如何基于HA存儲結構自動生成其Kripke結構；如何基于Kripke結構和EMC思想的檢測規則實現算法。下面將圍繞上述三個主要問題對檢測算法生成進行探討。

2 HA的自動生成

2.1 HA的邏輯結構

當系統比較復雜時，其狀態圖的往往代表多個對象的狀態行為，并且對象之間的狀態通過事件互相影響。如圖1所示在系統內部，狀態S1內仍有狀態轉換，此說明系統內初始運行對象的狀態轉換，例如當通過事件r1由S1內子狀態S6跳轉S2時，那么就是系統內S2所代表的另一個對象開始工作。從上述描述可以看出，系統狀態圖內具有明顯的層次關系，按照其層次關系轉換為HA（如圖2所示）。其邏輯結構各個順序自動機之間關系與樹的結點之間關系相同，例如：順序自動機A0其為根自動機，其無父狀態，只有一個根自動機，具有樹只有一個根結點的特征；除根自動機外，其他順序自動機A1和A2只有一個父狀態s1與之相對應，與樹中每個結點只有一個雙親結點相同；同一個父狀態的順序自動機互為兄弟。如果將HA的每個順序自動機看成結點，那么按照傳統樹的結點間的關系每個順序自動機的雙親結點應該同樣是一個順序自動機，但是順序自動機的雙親是某個順序自動機中的狀態?；诖朔N區別，順序自動機的在雙親結點包括了其父狀態及父狀態所屬的順序自動機。由于每個結點內是一個順序自動機，即一個狀態圖，因此結點內的結構可以采用有向圖的結構：每一個狀態就是一個頂點，狀態間的遷移關系即頂點間的鄰接關系，狀態件遷移事件即有向圖中頂點間的權值。綜上所述，HA的層次關系基于樹結構描述，順序自動機基于有向圖結構描述。

2.2 HA的存儲結構

HA的每個狀態其子順序自動機的數量沒有限制，即樹中每個結點其孩子結點數量沒有限制，需要選擇的存儲方式能夠在統一結點存儲結構的情況下，存儲每個結點和所有孩子結點之間的關系?；谏鲜鲈?，采用孩子兄弟表示法即二叉鏈表，同二叉樹的存儲結構一致，此種方法通過每個結點只記錄其第一個孩子，通過其孩子記錄兄弟的方式記錄所有的孩子結點。順序自動機的有向圖存儲結構要存儲狀態、每個狀態間的遷移關系及遷移事件。采用有向帶權矩陣，每個元素即遷移事件，無遷移關系的狀態對應的矩陣元素為0。

3 Kripke自動生成

3.1 關鍵問題

Kripke結構的M（SH，S0，R，L）定義，SH的生成是首要關鍵問題。SH是格局并配以格局內某狀態的遷移事件，因此先生成格局，再根據格局中的狀態遍歷每個狀態的遷移事件，從而生成SH。由于HA的存儲結構基于樹及圖，因此基于樹和圖的遍歷生成SH，其基本思想是：根順序自動機圖的深度遍歷開始，對正在訪問的某個狀態從左至右遍歷的前序遍歷的每一棵子順序自動機，生成格局；遍歷每個格局所有狀態的順序自動機的有向帶權矩陣，生成SH。例如，如圖2，從根順序自動機A0應用圖的深度遍歷，訪問狀態s1后，遍歷其子順序自動機A1和A2，每次各從其自動機中取出一個狀態，生成不同的狀態組合，從而生成了s1所屬的所有格局，C0={s1，s6，s8}， C1={s1，s6，s9}， C2={s1，s7，s8}， C3={s1，s7，s9}；其后，回溯至根順序自動機A0，訪問狀態s4和s5，生成格局C4={s2}，C5={s3}。Kripke生成的第二個關鍵問題為S0，S0為Kripke的初始狀態，其格局為初始格局C0，但是遷移事件不固定，可以默認包含C0的第一個狀態為初始狀態。R代表的是SH之間的遷移關系，受到所處格局和遷移事件影響，例如狀態S0其格局C0狀態包括{s1，s6，s8}，其遷移事件e1，根據狀態圖遷移關系為

，S0可遷移包括格局A2的狀態S7、S8及S9。R的遷移關系中遷移事件已經包含在狀態內，所以Kripke狀態間的遷移關系可以通過鄰接矩陣存儲。L為每個狀態原子命題集合，為該HA具備的所有基本性質，每個狀態的基本性質，即在該狀態的格局和遷移關系下滿足的基本性質，例如圖2Kripke狀態S0滿足其格局C0內所有狀態在遷移事件e1影響下的基本性質，即只有格局C0中只有狀態s6發生遷移，其他未變，此類性質如何保存成為關鍵。為每個Kripke狀態建立一個L，例如S0的集合L0，建立一個鄰接表，其格局C0所有狀態的遷移情況進行記錄，包括了其順序自動機內遷移狀態及遷移的Kripke狀態，其生成過程，可以在生成R時同時進行。

3.2 算法

輸入：HA存儲結構

輸出：HA的Kripke結構

1.定義格局數組C[MAX] [MAX]，初始化為空，其長度CLength初始化為0，k初始化為0；

2.定義Kripke狀態數組S[MAX]，其長度SLength初始化為0，l初始化為0；

3.深度優先遍歷HA的根順序自動機A[0]

（1）root=A[0].VERTEX[K]，棧s初始化為空；

（2）循環直到root為空且棧為空

a.循環直到root為空

將root保存到棧中；

繼續遍歷root的左子樹順序自動機頂點VERTEX[i]，i=i+1；

b.如果棧s不為空，則

如果root的右子樹為空，循環讀取棧的元素輸入到C[k][MAX]數組，k=k+1；

彈出棧頂元素至root；

準備遍歷root的右子樹順序自動頂點VERTEX[j]；

4.CLength=k，k=0；

5.循環直到k=CLength

（1）循環直到C[k] [MAX]為空

a.j初始化為0；

b.遍歷狀態C[k] [j]的有向帶權矩陣arc所處m行

S[l].C= C[k] [MAX]， S[l].E=arc[m][j]；

j++，l++；

（2） k++；

6. SLength=l，l=0；

7. R[SLength][SLength]數組初始化為0， L[SLength]初始化為空

8.循環直到l=SLength

（1） m=0；

（2）循環直到S[l]找到所有遷移狀態

a. S[m]如果是S[l]遷移狀態，R[m][l]=1；

b. 將此命題相關原子命題記錄L[l]

c.m++

（3） l++；

4 檢測規則的算法生成

已在文獻[3]中提出了基于LTL和CTL的檢測規則，這里不重復描述，主要討論基于此規則和HA的Kripke存儲結構的算法生成相關問題。檢測規則算法生成中的首要關鍵問題命題如何輸入表示，命題在初始輸入時，分解輸入，存入命題數組P[n]。 每個命題單元p[i]包括表達式包括五部分： p[i].no（是否非運算）、p[i].Sout（遷出狀態）、p[i].E（遷移事件隊列）、p[i].Sto（遷入狀態）、p[i].logic（邏輯運算符）。其次是每個命題單元如何分解成原子命題的形式，可以通過遷移事件隊列從Sout進行逐步遷移分解。最后，如果發現新的命題成立記錄LP[MAX][MAX]數組中，便于后續幫助其他命題判斷。具體算法如下：

輸入：HA的Kripke存儲結構，命題P[n]，成立命題LP[MAX][MAX]

輸出：命題是否成立

1. 遍歷LP[MAX][MAX]看是否存在P[n]，若存在結束；

2. i初始化為0，flag[n]初始化為1；

3.循環直到i=n；

（1） C= p[i].Sout的格局；

（2） e=p[i].E；

（3） 循環直到e為空

a.遍歷C格局的所有狀態遷移事件，若e不存在、p[i].no=1則結束當前循環， 若e不存在且e且p[i].no=0且flag[i]=0結束當前循環；

b.C=經過e遷入格局

c.e=p[i].E出隊事件；

4.，flag[n]之間用將p[n].logic連接計算，若結果為1，P[n]存入LP[MAX][MAX]；

5.輸出結果。

5 總結

在以往的相關文獻中提出了基于Kripk的復雜演繹判斷規則及形式化語義推導的理論，但較少給出實際算法，缺乏實用性。針對上述問題，基于已提出的檢測規則，從存儲結構HA定義、Kripke結構生成及基于Kripke結構檢測規則算法實現進行討論，給出了具體存儲結構及算法，算法易于理解與實現，具有非常重要的實際意義。

參考文獻

[1]Latella D，Majzik I，Massink M. Towards a formal operational semantics of UML Statechart diagrams.In：Ciancarini P， Fantechi A，Gorrieri R，eds.Proceedings of the 3rd International Conference on Formal Methods for Open Object-Oriented Distributed Systems. Boston：Kluwer Academic Publishers， 1999：15-18.

[2]邊計年，薛宏熙，蘇明，吳為民.數字系統設計自動化[M].北京：清華大學出版社，2005（07）.

[3]王佳婧.基于EMC和HA的UML Statecharts檢測研究[J].通訊世界，2017（16）.

作者簡介

王佳婧（1982-），女，吉林省吉林市人。碩士學位。現為吉林動畫學院講師。研究方向為計算機應用技術。

作者單位

吉林動畫學院 吉林省長春市 130012