接口自動機的良構性檢測算法及其實現

李 雪，朱嘉鋼

(江南大學 物聯網工程學院，江蘇 無錫 214122)

(*通信作者電子郵箱jndx_axue@163.com)

接口自動機的良構性檢測算法及其實現

李 雪*，朱嘉鋼

(江南大學 物聯網工程學院，江蘇 無錫 214122)

(*通信作者電子郵箱jndx_axue@163.com)

針對構件式系統中任一構件的非良構性會導致系統不能正常運行的問題，提出一種基于接口自動機(IA)來分析和檢測構件良構性(well-formedness)的算法，并據此實現了一個構件良構性檢測原型系統。該算法首先構造與接口自動機同構的可達圖；其次，基于可達圖通過深度優先遍歷生成一條覆蓋所有遷移的有序集；最后，根據該有序集檢測在外界環境滿足其輸入假設的情況下，每個屬于方法的活動到其對應返回活動的路徑的自治無異常可達性，從而實現接口自動機的良構性檢測。根據所提算法在Eclipse平臺設計并實現了構件良構性檢測原型系統T-CWFC，該系統通過JFLAP建立構件的接口自動機模型并構造其可達圖，進而對接口自動機作良構性檢測并輸出相關檢測信息。最后通過對一組構件的良構性檢測實驗驗證了算法的有效性。

接口自動機；構件；良構性；最簡運行

0 引言

在軟件開發過程中，基于構件的設計已成為處理復雜系統、提高生產力和產品質量的一個重要途徑。構件封裝特定功能，并通過接口(interface)來與構件式系統中的其他構件實現通信。在構建構件式系統時，對參與組合的構件的功能性和非功能性進行分析檢測，是提高系統可靠性的有效途徑之一。在檢測已發現構件、重構的構件的良構性時，若發現其為非良構的，則必須拒絕其參與系統的構造[1]。為此，在組合構件系統、替換或細化現有構件式系統中的某個構件時，為使替換后系統正常運行，判斷構件的良構性是必要的。

在構件良構性相關研究方面，諸多學者都作了有益的工作。文獻[2]給出了良構性定義，認為接口是良構的，只要存在一種可以按照某種方式來適當選擇其為接口所提供的輸入來避免系統到達所有非法狀態的環境時，即構件接口在其某個內部狀態上不能接受某個輸入時，外界環境不為其提供該輸入[2]。該思想認為接口自動機(Interface Automaton, IA)是否是良構的，取決于是否存在一個合適的環境能夠滿足構件接口的所有輸入假設而使非法狀態不會達到，而未考慮在外界環境滿足其輸入假設時，接口自身內部的良構性。文獻[3]采用著色Petri網對Web服務進行建模，并在工作流網“良構性”定義基礎上給出Web服務良構性定義，并指出服務的良構性能夠保證組合服務可達終止狀態的正確性。文獻[4]基于Petri網給出了服務流程是良構的當且僅當其具有活性和有界性。文獻[5]通過為接口自動機中每個狀態添加時鐘變量實現對具有實時特性的構件進行建模，并在文獻[6]中提出的良構性基礎上增加了時間良構性約束條件。文獻[7]則通過擴大接口自動機中自治活動的范圍，在考慮外界環境滿足構件需求的情況下，給出了接口自動機良構性的定義，即其與環境交互時接口內部自身能夠正確運行而不會一直停留在某一狀態，并指出當參與組合的接口自動機是良構的且其語義兼容時，則其組合系統也是良構的。但是，這些研究均未給出構件良構性的具體檢測算法，只能由開發者自行根據定義描述來判定，降低了開發效率。

為此，本文首先提出了檢測接口自動機良構性的算法。該算法利用接口自動機的可達圖[8]，通過深度優先遍歷算法遍歷可達圖獲取一條覆蓋所有遷移的簡單有序集，然后依次尋找有序集中每個方法活動到其對應返回活動間的最簡運行并檢測其自治無異常可達性，從而實現接口自動機良構性檢測。當接口自動機中每個方法活動到其對應返回活動都是自治無異常可達的，則可得出該接口自動機是良構的。基于所提出的良構性檢測算法，在Eclipse平臺中實現了一個構件良構性的檢測工具(Tool for Component Well-Formedness Checking，T-CWFC)。該檢測工具的原型系統包括接口自動機建模模塊、輸入模型處理模塊、構造可達圖并獲取簡單有序集模塊以及良構性檢測和結果輸出模塊。最后，用上述原型系統對一組構件作良構性檢測，得到了預期的結果，說明所提出的算法是有效的。

1 構件建模及其良構性

構件是一個包含提供接口和需求接口的軟件單元[9]。構件的粒度可大可小，可以是一個類也可以是一個服務[10]。構件僅通過這些接口來與環境進行交互，因此常采用對接口進行形式化描述的方法來刻畫構件的交互特性。本文采用接口自動機對構件進行建模，進而分析檢測其良構性。

1.1 接口自動機及其良構性

傳統的接口自動機理論將構件中的每個活動看作是一個輸入、輸出或內部活動。在刻畫活動的語義信息時，文獻[7]將每個活動進一步細化為方法活動、返回活動和異常活動等三種類型，并給出了接口自動機良構性定義。

為了描述方便，本文用符號“a?”“a!”和“a;”分別表示輸入活動、輸出活動和內部活動，其中a為活動名。類似地，用符號“m”“r”和“e”分別表示活動類型為方法類型、返回類型和異常類型。IA的形式化定義如下。

定義2 運行和可達的(run and reachable)[6]。接口自動機P中的運行是狀態和動作的有限交替序列v0,a0,v1,a1,…,vn且對于所有的i(0≤i

定義3中的符號Succp(v,a)代表狀態v接收到活動a后能夠到達的狀態。定義3認為構件在與環境交互過程中，只要其能夠接收各個方法活動的返回活動時，接口自動機中存在一條可控且能夠無異常到達使能其返回活動的狀態的運行即認為接口自動機是良構的。

1.2 最簡運行和自治無異常可達

在構件式系統中，對于任一構件，系統中的其他構件可看作是其工作環境。接口自動機描述了構件接口的時序特性，同時將接口的輸出保證和輸入假設整合在一起，其中輸出保證相當于接口對環境所作的假設；輸入假設則相當于接口自身行為的一種描述[2]。外界環境總是能夠滿足其要求，即當P需要接收(或發送)消息時，外界環境總是能夠適時地發送(或接收)該消息，從而能夠排除因外界環境導致接口自動機中運行出現死鎖的情況[3]。

由定義3可知，在外界環境滿足其輸入假設時，檢測構件的良構性需要：1)首先找到Succp(v,a)到使能其返回活動Rp(a)的狀態u∈VP之間的運行；2)判斷該運行中包含的活動是否是自治無異常的。然而，當接口自動機P中存在環路或存在多次調用方法活動a時，狀態v和使能Rp(a)的狀態u之間的運行路徑將隨著環路執行的次數不同而可能使兩狀態間的運行數目和運行所經過的狀態數是無窮的、不確定的。在此，為了檢測構件的良構性，本文考慮兩狀態間的最簡運行來保證運行中不會出現循環執行某一個環路的情況，從而使狀態v到u的運行數目具有確定性，運行長度具有最短性。

定義4 最簡運行(thesimplerun)。對于接口自動機P中狀態vi與vj間的運行η=viaivi+1…vj-1aj-1vj且(i

定義4是在定義2的基礎上，對運行中的環路和運行長度添加了限制條件。特別地，用集合Ση表示最簡運行η中所有被使能的活動ai,ai+1,…,aj-1。

另外，文獻[7]根據對活動的不同分類將兩狀態間的運行分為自治運行(autonomousrun)和非自治運行(non-autonomousrun)。由此兩狀態間的可達性可分為自治可達(reachableautonomously)和非自治可達(reachablenon-autonomously)。為了方便下文中形式化描述構件良構性檢測，結合定義2和4給出了最簡自治無異常可達定義。

文獻[7]中將每個方法活動的返回值細分為返回活動和異常活動兩種。由此，文獻[6]所給出的通信構件User的輸出保證，即對外界所作的假設為環境提供了方法活動msg，并在User調用方法活動msg時，給出相應的通信成功ok和通信失敗fail信息。而構件User并未對通信失敗活動fail有任何響應，則認為User的外部環境不能滿足其輸入假設。此時構件User在與其環境組合時依然會因非同步活動而引入非法狀態。

以上的條件1)描述了構件中方法活動的返回活動或異常活動不在構件可接受范圍之內的情形，即外界環境不滿足構件的輸入假設。條件2)和3)描述了構件在輸入假設滿足的情況下，不能滿足方法活動到使能其返回活動的狀態是可控且能夠到達的情形，即構件會一直停留在某一狀態而使構件失效。

接口自動機的組合參考文獻[6]定義10所描述的接口自動機組合方法，關于良構的接口自動機及其組合的一個重要結論如下:設兩個接口自動機分別為P1和P2，P1和P2能夠組合且其組合為P=P1‖P2，若接口自動機P1和P2是良構的，則其組合P是良構的。

2 良構性檢測算法實現

通過1.2節對構件良構性檢測的幾種情況的分析可知，在外界環境滿足其輸入假設時，為檢測構件的良構性，首先需要獲取從方法活動到使能其返回活動的狀態間的運行；其次，判斷該運行是否是自治無異常的。下面將分別給出具體實現算法。

2.1 獲取兩狀態間運行方法

文獻[8]中在驗證構件式系統與需求規約的一致性時，為獲取構件式系統的任一行為，給出了構造與構件式系統同構的可達圖的方法，并證明了構件式系統的任一行為都會對應可達圖中的一條路徑。然而，當可達圖中存在環路，此時路徑的數目可能是無窮的，路徑的長度也可能是無窮的[8]。為此，本文首先構造與IA同構[11]的可達圖，其次通過深度優先遍歷(Depth-FirstSearch，DFS)來實現自動生成一條覆蓋自動機中所有遷移且不包含重復遷移的有序集，最后根據有序集獲取任意兩狀態間的運行。可達圖的構造方法見文獻[8]。

在采用DFS方法遍歷圖的過程中，碰到環路且判定當前節點已訪問過時，便回溯，此時環路中的部分轉換邊則會在有窮的遍歷中被漏掉。為解決上述問題，本文引入簡單有序集的概念，并給出通過DFS遍歷G得到簡單有序集的實現算法，見算法1。

對于可達圖G=(V,T)，且其有窮邊集T的個數為NumT，通過DFS遍歷得到的任一條有序集P=t0t1…tn是簡單有序集，若有序集P同時滿足：1)對于任何i,j(0≤i

算法1DFS遍歷邊序列生成算法。

輸入 可達圖G=(V,T),V≠?,T≠?。

輸出R={〈vi,af,vj〉k|k滿足對G的DFS順序}。

1)

初始化：G′=(V′,T′)?G,R??,k?1;

2)

vt1?v0∈V′;

//取出第一個頂點

3)

4)

vt1?v′i，轉3)；

5)

結束。

2.2 構件良構性檢測算法

通過2.1節引入的簡單有序集概念，將采用DFS遍歷可達圖時可能得到的有序集的個數和有序集長度均限制在有窮有序集中。此時，根據該有序集檢測構件良構性則需要循環依次檢測有序集中每個方法活動到使能其返回活動的狀態是否是可達的且是自治無異常可達的。根據1.2節可知，在檢測構件的良構性時，需獲取該兩狀態間的最簡運行。而根據算法1得到的有序集有可能包含環路的和不連續的，為此首先需要將兩狀態間的有序集化簡為最簡運行，然后根據最簡運行來檢測從方法活動是否能夠自治無異常地到達使能其返回活動的狀態。為此，本文給出將兩狀態間的簡單有序集化簡為最簡運行的方法。

設遍歷G得到的有序集path中任意兩個節點vi和vj間存在一個有序集η=(vi,ai,vi+1) (vm,am,vm+1)… (vj-1,aj-1,vj)，且η不是最簡運行，則執行以下步驟將其化簡成最簡運行：

1)對η中任意相鄰轉換邊(vp,ap,vp+1)(vq,aq,vq+1),若vp+1≠vq，則取path中起始節點為vp+1，終止節點為vq之間的有序集添加至η中的該相鄰轉換邊之間，得到有序集η′；

2)路徑η′中，對于任意m,n(i≤m

3)重復1)和2)，直到有序集η是最簡運行。

算法2 構件良構性檢測算法。

輸出 構件是否為良構的布爾值isWell；構件為非良構時的錯誤記錄rst。

1)

初始化：k?1,flag?true,isWell?false,rst??;at?null,ae?null，run??,N?|R|;M?|run|；

2)

檢測每個mi到對應ri的自治無異常可達性：

a)

b)

若存在i滿足af=mi且〈mi,ri,ei〉∈ΣflagP，則

c)

at?ri；ae?ei;

d)

若〈vi′,at,vj′〉∈R且〈vi″,ae,vj″〉∈R，則

e)

若t≥k則run?{〈vi,af,vj〉x|k≤x≤t};

f)

否則run?{〈vi,af,vj〉x-k+1|k≤x≤N}∪{〈vi,af,vj〉x+N-k+2|0≤x≤t};

g)

否則flag?false;rst?rst∪{at,ae},轉o);

h)

對run進行去環操作，使run滿足：對于任意〈vi,ax,vj〉∈R，均不存在另一個〈vi′,ax′,vj′〉∈R，使得vi=vi′；

i)

對run進行連接操作，使run滿足：對于任意〈vi,ax,vj〉∈R′，若存在右側相鄰〈vi′,ax′,vj′〉∈R′，有vj=vi′;

j)

重復執行一次步驟h)、i);

k)

取ax滿足〈vi,ax,vj〉∈run;

l)

若ax?Σaut_noExcP,則flag?false，rst?rst+{ax?Σaut_noExcP};

m)

x?x+1;

n)

若x≤M,則轉k)；

o)

k?k+1;

p)

若k≤N，則轉2);

3)

若flag=true則isWell?true;

否則isWell?false；

4)

結束。

算法2中的步驟2)則是依次取出有序集R′中的每個元組〈vi,ak,vj〉，并在環境滿足構件的輸入假設時，判斷R′中方法活動mi到其對應返回活動ri之間的自治無異常可達性。其中，步驟c)～f)則為方法活動對應的返回活動滿足構件的輸入假設時，在有序集R′中取出方法操作與其返回活動間的有序集run；步驟h)～j)則是根據2.2節介紹的最簡運行化簡方法，將已獲取的有序集run化簡為最簡運行；步驟k)～n)則是循環檢測最簡運行run中每個元組所包含的活動是否是自治無異常活動，若其中任意一個活動不是自治操作則布爾值flag為false，從而實現在算法結束時根據flag值來判定構件的良構性。

在該良構性檢測過程中，在外界環境滿足構件的輸入假設時，只要兩節點間的最簡運行不符合良構性定義3則該接口自動機即為非良構的。因文中引入了最簡運行概念，所以遍歷與IA模型同構的可達圖時，得到的簡單有序集長度是有限的，則算法2是可終止的，且其算法復雜度隨G中節點數和方法活動個數的增加而增加。

3 良構性檢測系統實現及實例應用

基于以上理論分析，本文設計了一個構件良構性檢測原型工具T-CWFC。該原型工具采用具有良好的跨平臺運行特征以及豐富的類庫資源的java作為工具的實現語言，并使用Eclipse的插件技術來設計和開發T-CWFC，因此，該工具易于在Eclipse環境中通過插件技術來安裝、配置和使用。T-CWFC的目的是應用于構件式軟件開發的設計建模階段，對構件的良構性進行形式化的分析和檢測，從而保證組合系統能夠正常運行，為系統的其他功能性分析和驗證等作準備。

3.1 良構性檢測系統實現

構件良構性檢測工具T-CWFC中模型分析和檢測基本流程如圖1所示(其中，黑色圓點節點為開始，矩形節點為系統的輸入和輸出)：首先對IA模型進行輸入處理；其次基于DFS算法分析得到覆蓋被測構件的IA模型中所有遷移的有序集；然后根據構件外界環境需求和有序集實現良構性檢測，最后給出檢測結果和相應錯誤報告。

圖1 T-CWFC的模型良構性檢測流程的活動圖

3.1.1IA模型輸入處理

接口自動機是有限自動機的擴展，是一種特殊的自動機[6]。JFLAP(JavaFormalLanguagesandAutomataPackage)[12]是一款Java語言編寫的開源工具，它不僅提供了方便易用的有限自動機建模接口，而且提供了在有限自動機中添加一些文本和標簽的功能。為此，本文采用JFLAP工具建模接口自動機模型并為接口自動機的每個操作添加相應的類型標簽，然后將保存得到的.jff文件作為T-CWFC的輸入。T-CWFC系統中，為獲取構件的簡單有序集，首先需對輸入進行解析，即對輸入.jff文件進行解析處理得到接口自動機的狀態、遷移、活動名和活動類型等信息。以下給出文獻[6]中通信構件User的接口自動機模型對應的.jff文件示例說明。其中：標簽標明該接口自動機為有限接口自動機；標簽則是建模時添加的標簽信息，即描述了系統環境和構件內部的方法活動和其相應返回活動、異常活動。

fa

176.0 117.0

299.0 119.0

1

0

ok?

0 1 msg!

outputmethod:msg,

inputreturn:ok,

inputexception:fail;

136.0 50.0

3.1.2 獲取簡單有序集

3.1.1節已通過解.jff文件在內存中創建了IA模型對象。為獲取包含IA模型的所有遷移且不具有重復遷移的有序集，本文采用文獻[8]中構建與接口自動機網絡同構的可達圖方法，逐個讀取已創建的數據結構State中的狀態信息來構建可達圖的頂點，并利用已創建的Transition和Action來創建可達圖中的各條邊，從而在內存中構造一個與接口自動機對象相對應的可達圖，進而采用DFS遍歷該可達圖得到一個簡單有序集。獲取可達圖中簡單有序集的流程如圖2所示。

圖2 簡單有序集獲取的流程

遍歷可達圖生成簡單有序集的算法見算法1。算法的輸出是一條簡單有序集，該簡單有序集形如(s0,m1,s1)→(s1,m2,s2)→…→(sp,mn,sq)，且mx(1≤x≤n)是IA中的動作，sx(1≤x≤q)是IA中的狀態。另外，在T-CWFC生成的有序集中，對每個遷移中包含的動作mx的類型也進行了詳細的標注，即明確標注其為方法“m”(或返回“r”或異常“e”)活動和輸入“?”(或輸出“！”或內部“；”)類型。

3.1.3 良構性檢測

由3.1.2節的分析可知，DFS遍歷可達圖時得到的有序集的個數和有序集長度均為有窮的。根據時序特性可知，無論IA中的內部狀態轉移是順序、選擇還是并行結構，接口自動機中每個方法活動執行之后，才會接收或發送其返回活動和異常活動，因此在接口自動機中不存在先使能返回或異常活動再使能其方法活動的情況出現。由此，根據3.1.1和3.1.2節得到的系統輸入和簡單有序集即可利用2.2節給出的算法2對構件的良構性進行檢測。

圖3給出了構件良構性檢測工具T-CWFC工具中IA模型良構性檢測的類圖框架。該類圖框架主要包括自動機模型核心類、構造與IA同構可達圖的Graph、Vertex和createGraph類、檢測良構性相關類(其包括wellFormedDetect class和dfsTraversal類)以及表示外界環境信息的Message類和解析jff文件的輔助工具類parJffTools class和parseInfo class。

在良構性檢測類(wellFormedDetect class)的實現過程中，其中一個關鍵的問題為：在判定IA模型的良構性時，需要首先獲取方法活動到其返回活動間的最簡運行，然后根據定義5來進行判定。而直接從dfsTraversal類得到的簡單有序集中獲取的兩狀態間的路徑有可能不是最簡運行。為此，在實現類wellFormedDetect時，本文系統首先根據2.2節給出的化簡方法將兩狀態間的路徑化簡為最簡運行，然后按照算法2實現良構性檢測，并給出良構性檢測的過程和結果報告。在實際中亦會出現構件中的同一方法活動發生兩次且其返回活動亦可能出現兩次的情況，則需要準確確定該方法活動與其相應返回活動的運行，本系統在實現過程中對這種情況也作了相應處理，從而保證構件良構性檢測的正確性。

圖3 T-CWFC中良構性檢測類圖

3.2 應用實例

本文設計和實現的T-CWFC模型檢測工具是在Windows 7活動系統平臺，eclipse 4.3.2、 java jdk 1.7和JFLAP 7.0環境下開發。本節以文獻[6]中所給出的通信構件Comp和User的接口自動機模型對T-CWFC模型檢測工具進行應用說明。

在JFLAP中建立的具有類型信息的構件Comp和User模型如圖4所示。其中，圖4(a)的IA模型描述了構件Comp在假設環境確定下與環境交互的行為特征：即其假設環境提供了send方法活動，且在該方法活動被調用時給出相應的返回活動ack和異常活動nack，所以當Comp中方法活動msg被外部調用時，構件將先調用send方法活動與其環境進行交互，并在接收環境提供的返回活動ack之后，向調用者返回通信成功信息ok；若連續兩次send請求活動接收到的都是一次活動nack，則向通信者返回通信異常fail。圖4(b)的IA模型描述了構件Comp的使用者構件User在假設環境確定下的行為特征，其對環境的假設為當其調用環境Comp提供的msg消息時，則會得到通信成功ok信息和通信異常fail信息。

圖4 通信構件的IA模型

根據良構性定義5就能從直觀上判斷Comp是良構的，而User對外界環境提供的通信異常活動無響應，在外界環境滿足其輸入假設時則是良構的。運行T-CWFC進行User和Comp良構性檢測的結果如圖5所示。其中:界面左邊的“JFLAP建模IA”按鈕則是利用有限自動機建模JFLAP插件用于對接口自動機進行建模;“選擇(IA)jff文件”則是選擇待檢測構件的建模文件;“良構性檢測”按鈕則是根據算法1和2檢測所選的jff文件的良構性，并在界面的右側文本區域顯示出檢測結果。

圖5 通信構件的T-CWFC運行界面

由圖5(a)中所給結果顯示構件User未對通信異常活動作出響應，具體檢測結果信息為：通過DFS遍歷其相應可達圖得到的簡單有序集為(s0,msg!m,s1)→(s1,ok?r,s0)，且對于方法活動msg達到的狀態s1到使能返回活動ok的狀態之間是自治無異常可到的。而對于構件User在初始狀態s0調用外部環境提供的方法活動msg后遷移到s1后，并未對外部環境提供的通信異常消息fail作出相應的響應，即當構件Comp的輸出信息fail是構件User的輸入時，構件User將一直停留在狀態s1。由此可見，運行T-CWFC檢測的結果與根據定義5得到的相同，即異常返回是不正確的結論。此時，在構件User與其他構件參與組合時，即可根據檢測得到的結果指導設計者提供合適的外界環境來滿足其輸入假設從而保證該構件是良構的。

圖4(b)顯示Comp的IA模型中存在三個環路，且從狀態s2和s4到初始狀態s0均分別有兩個選擇分支，則對Comp對應的可達圖進行DFS遍歷時共有四條簡單有序集。圖5(b)顯示運行T-CWFC得到的簡單有序集(s0,msg?m,s1)→(s1,send!m,s2)→(s2,nack?e,s3)→(s3,send!m,s4)→(s4,nack?e,s6)→(s6,fail!e,s0)→(s4,ack?r,s5)→(s5,ok!r,s0)→(s2,ack?r,s5)是DFS遍歷可得到的。對于構件Comp中提供的方法活動msg，從圖4(b)可分析出使能其返回活動ok的狀態為s5，且從s1到s5的最短路徑為(s1,send!m,s2)→(s2,ack?r,s5)。圖5(b)的結果顯示，方法活動msg到使能返回活動ok之間的簡單有序集為(s1,send!m,s2)→(s2,nack?e,s3)→(s3,send!m,s4)→(s4,nack?e,s6)→(s6,fail!e,s0)→(s4,ack?r,s5)→(s5,ok!r,s0)→(s2,ack?r,s5)，該有序集所包含的遷移中存在具有相同起始狀態的遷移，且其中的部分相鄰的兩個遷移中存在前一個遷移的終止狀態不等于后一個遷移的起始狀態的情況，即DFS遍歷得到的有序集中存在環路和不連續遷移，按2.2節的最簡路徑化簡方法去除環路并將不連續的路徑變成連續得到的最簡運行為(s1,send!m,s2)→(s2,ack?r,s5)，根據定義4可知，從s1到s5是自治無異常可達的。

同理，圖5(b)的運行結果顯示：首次調用方法活動send的終止狀態s2到使能其返回活動的s2的運行和化簡后的運行、第二次調用方法活動send的終止狀態s4到使能其返回活動的s4均與實際分析得到的相同，且發現該兩種方法活動到達的狀態與使能其返回活動的狀態相同，即自治無異常可達的。

利用本文提出的算法2對構件Comp和User的良構性檢測已結束，且其檢測結果與分析結果是一致的。由此可見，本文提出的基于接口自動機的構件良構性判定算法是有效的。

4 結語

本文基于接口自動機理論給出了一種檢測構件良構性的算法，并根據該算法在Eclipse平臺設計并實現了檢測構件良構性的原型工具T-CWFC。該工具可應用于構件式系統軟件開發的設計建模階段，對參與組合系統的構件的自身良構性進行分析和檢測，有助于設計者盡早發現錯誤并采取相應措施予以修正處理，從而實現一次性正確構造系統來降低成本并提供系統可靠性。本文只給出了檢測參與組合構件的良構性檢測算法，后續工作中則將對該原型工具T-CWFC繼續完善，以加入構件式系統的其他功能性測試等。

References)

[1] STEIMANN F.From well-formedness to meaning preservation: model refactoring for almost free [J].Software & Systems Modeling, 2015, 14(1): 307-320.

[2] 張巖,胡軍,于笑豐,等.接口自動機——一種用于組件組合的形式系統[J].計算機科學,2005,32(11):212-217.(ZHANG Y, HU J, YU X F, et al.Interface automata — a formal system for components composition [J].Computer Science, 2005, 32(11): 212- 217.)

[3] 李喜彤,范玉順.Web服務流程相容性和相似性分析[J].計算機學報, 2009, 32(12):2429-2437.(LI X T, FAN Y S.Analyzing compatibility and similarity of Web service processes [J].Chinese Journal of Computers, 2009, 32(12): 2429-2437.)

[4] REISIG W.Well-formed system nets [M]// Understanding Petri Nets.Berlin: Springer-Verlag, 2013: 169-172.

[5] DE ALFARO L, HENZINGER T A, STOELINGA M, et al.Timed interfaces [C]// EMSOFT 2002: Proceedings of the 2nd International Conference on Embedded Software, LNCS 2491.Berlin: Springer-Verlag, 2002: 108-122.

[6] DE ALFARO L, HENZINGER T A.Interface automata [J].ACM SIGSOFT Software Engineering Notes, 2001, 26(5): 109-120.

[7] MOUELHI S, AGROU K, CHOUALI S, et al.Object-oriented component-based design using behavioral contracts: application to railway systems [C]// CBSE ’15: Proceedings of the 18th International ACM Sigsoft Symposium on Component-Based Software Engineering.New York: ACM, 2015: 49-58.

[8] HU J, YU X, WANG L, et al.Scenario-based specifications verification for component-based embedded software designs [C]// ICPPW ’05: Proceedings of the 2005 International Conference on Parallel Processing Workshops.Washington, DC: IEEE Computer Society, 2005: 240-247.

[9] SHAI O, PREISS K.Isomorphic representations and well-formedness of engineering systems [J].Engineering with Computers, 1999, 15(4): 303-314.

[10] 雷斌,王林章,卜磊,等.基于狀態機模型的構件健壯性測試[J].軟件學報,2010,21(5):930-941.(LEI B, WANG L Z, BU L, et al.Robustness testing for components based on state machine model [J].Journal of Software, 2010, 21(5): 930-941.)

[11] 王文霞.有向圖的同構判定算法:出入度序列法[J].山西大同大學學報(自然科學版),2014,30(2):10-13.(WANG W X.An isomorphism testing algorithm for directed graphs: the in-degree and out-degree sequence method [J].Journal of Shanxi Datong University (Natural Science Edition), 2014, 30(2):10-13.)

[12] RODGER S H, FINLEY T W.Jflap: An Interactive Formal Languages and Automata Package [M].Sudbury: Jones & Bartlett Publishers, 2006: 1-15.

This work is supported by Industry-University-Research Project of Jiangsu Province (BY2013015- 40).

LI Xue, born in 1990, M.S.candidate.Her research interests include software engineering, formal method.

ZHU Jiagang, born in 1957, Ph.D., professor.His research interests include artificial intelligence, pattern recognition, software engineering.

Well-formedness checking algorithm of interface automaton and its realization

LI Xue*, ZHU Jiagang

(CollegeofIoTEngineering,JiangnanUniversity,WuxiJiangsu214122,China)

To address the issue that the non-well-formed components in a component-based system may lead to the whole system working abnormally, an algorithm for checking the well-formedness of a component was proposed based on its Interface Automaton (IA) model, and a relevant prototype tool was developed.Firstly, the reachability graph isomorphic with the given IA was constructed.Secondly, an ordered set including all the transitions of the reachability graph relevant to the IA was obtained by depth-first-searching the reachability graph.Finally, the well-formedness check of a given IA was completed by checking whether each action belonging to a method in the IA could autonomously reach its return action without exception according to the ordered set under the condition that the external environment meets the input hypothesis.As a realization of the proposed algorithm, a relevant prototype tool was developed on Eclipse platform, namely T-CWFC (Tool for Component Well-Formedness Checking).The prototype tool can model the given component, set up its reachability graph, check its well-formedness and output check result message.The validity of the proposed algorithm was verified by running the tool on a set of components.

Interface Automaton (IA); component; well-formedness; the most simple run

2016- 07- 22;

2016- 08- 28。 基金項目:江蘇省產學研項目(BY2013015- 40)。

李雪(1990—)，女，河南南陽人，碩士研究生，主要研究方向：軟件工程、形式化方法； 朱嘉鋼(1957—)，男，上海人，副教授，博士，主要研究方向：人工智能、模式識別、軟件工程。

1001- 9081(2017)02- 0574- 07

10.11772/j.issn.1001- 9081.2017.02.0574

TP311

A