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其為根自動機，其無父狀態，只有一個根自動機，具有樹只有一個根結點的特征；……