接口自動機(jī)的良構(gòu)性檢測算法及其實現(xiàn)

李 雪，朱嘉鋼

(江南大學(xué) 物聯(lián)網(wǎng)工程學(xué)院，江蘇 無錫 214122)

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

接口自動機(jī)的良構(gòu)性檢測算法及其實現(xiàn)

李 雪*，朱嘉鋼

(江南大學(xué) 物聯(lián)網(wǎng)工程學(xué)院，江蘇 無錫 214122)

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

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

接口自動機(jī)；構(gòu)件；良構(gòu)性；最簡運(yùn)行

0 引言

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

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

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

1 構(gòu)件建模及其良構(gòu)性

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

1.1 接口自動機(jī)及其良構(gòu)性

傳統(tǒng)的接口自動機(jī)理論將構(gòu)件中的每個活動看作是一個輸入、輸出或內(nèi)部活動。在刻畫活動的語義信息時，文獻(xiàn)[7]將每個活動進(jìn)一步細(xì)化為方法活動、返回活動和異?；顒拥热N類型，并給出了接口自動機(jī)良構(gòu)性定義。

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

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

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

1.2 最簡運(yùn)行和自治無異?？蛇_(dá)

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

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

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

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

另外，文獻(xiàn)[7]根據(jù)對活動的不同分類將兩狀態(tài)間的運(yùn)行分為自治運(yùn)行(autonomousrun)和非自治運(yùn)行(non-autonomousrun)。由此兩狀態(tài)間的可達(dá)性可分為自治可達(dá)(reachableautonomously)和非自治可達(dá)(reachablenon-autonomously)。為了方便下文中形式化描述構(gòu)件良構(gòu)性檢測，結(jié)合定義2和4給出了最簡自治無異?？蛇_(dá)定義。

文獻(xiàn)[7]中將每個方法活動的返回值細(xì)分為返回活動和異?；顒觾煞N。由此，文獻(xiàn)[6]所給出的通信構(gòu)件User的輸出保證，即對外界所作的假設(shè)為環(huán)境提供了方法活動msg，并在User調(diào)用方法活動msg時，給出相應(yīng)的通信成功ok和通信失敗fail信息。而構(gòu)件User并未對通信失敗活動fail有任何響應(yīng)，則認(rèn)為User的外部環(huán)境不能滿足其輸入假設(shè)。此時構(gòu)件User在與其環(huán)境組合時依然會因非同步活動而引入非法狀態(tài)。

以上的條件1)描述了構(gòu)件中方法活動的返回活動或異?；顒硬辉跇?gòu)件可接受范圍之內(nèi)的情形，即外界環(huán)境不滿足構(gòu)件的輸入假設(shè)。條件2)和3)描述了構(gòu)件在輸入假設(shè)滿足的情況下，不能滿足方法活動到使能其返回活動的狀態(tài)是可控且能夠到達(dá)的情形，即構(gòu)件會一直停留在某一狀態(tài)而使構(gòu)件失效。

接口自動機(jī)的組合參考文獻(xiàn)[6]定義10所描述的接口自動機(jī)組合方法，關(guān)于良構(gòu)的接口自動機(jī)及其組合的一個重要結(jié)論如下:設(shè)兩個接口自動機(jī)分別為P1和P2，P1和P2能夠組合且其組合為P=P1‖P2，若接口自動機(jī)P1和P2是良構(gòu)的，則其組合P是良構(gòu)的。

2 良構(gòu)性檢測算法實現(xiàn)

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

2.1 獲取兩狀態(tài)間運(yùn)行方法

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

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

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

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

輸入 可達(dá)圖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，轉(zhuǎn)3)；

5)

結(jié)束。

2.2 構(gòu)件良構(gòu)性檢測算法

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

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

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

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

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

算法2 構(gòu)件良構(gòu)性檢測算法。

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

1)

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

2)

檢測每個mi到對應(yīng)ri的自治無異常可達(dá)性：

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},轉(zhuǎn)o);

h)

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

i)

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

j)

重復(fù)執(zhí)行一次步驟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,則轉(zhuǎn)k)；

o)

k?k+1;

p)

若k≤N，則轉(zhuǎn)2);

3)

若flag=true則isWell?true;

否則isWell?false；

4)

結(jié)束。

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

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

3 良構(gòu)性檢測系統(tǒng)實現(xiàn)及實例應(yīng)用

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

3.1 良構(gòu)性檢測系統(tǒng)實現(xiàn)

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

圖1 T-CWFC的模型良構(gòu)性檢測流程的活動圖

3.1.1IA模型輸入處理

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

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節(jié)已通過解.jff文件在內(nèi)存中創(chuàng)建了IA模型對象。為獲取包含IA模型的所有遷移且不具有重復(fù)遷移的有序集，本文采用文獻(xiàn)[8]中構(gòu)建與接口自動機(jī)網(wǎng)絡(luò)同構(gòu)的可達(dá)圖方法，逐個讀取已創(chuàng)建的數(shù)據(jù)結(jié)構(gòu)State中的狀態(tài)信息來構(gòu)建可達(dá)圖的頂點，并利用已創(chuàng)建的Transition和Action來創(chuàng)建可達(dá)圖中的各條邊，從而在內(nèi)存中構(gòu)造一個與接口自動機(jī)對象相對應(yīng)的可達(dá)圖，進(jìn)而采用DFS遍歷該可達(dá)圖得到一個簡單有序集。獲取可達(dá)圖中簡單有序集的流程如圖2所示。

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

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

3.1.3 良構(gòu)性檢測

由3.1.2節(jié)的分析可知，DFS遍歷可達(dá)圖時得到的有序集的個數(shù)和有序集長度均為有窮的。根據(jù)時序特性可知，無論IA中的內(nèi)部狀態(tài)轉(zhuǎn)移是順序、選擇還是并行結(jié)構(gòu)，接口自動機(jī)中每個方法活動執(zhí)行之后，才會接收或發(fā)送其返回活動和異?；顒?，因此在接口自動機(jī)中不存在先使能返回或異常活動再使能其方法活動的情況出現(xiàn)。由此，根據(jù)3.1.1和3.1.2節(jié)得到的系統(tǒng)輸入和簡單有序集即可利用2.2節(jié)給出的算法2對構(gòu)件的良構(gòu)性進(jìn)行檢測。

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

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

圖3 T-CWFC中良構(gòu)性檢測類圖

3.2 應(yīng)用實例

本文設(shè)計和實現(xiàn)的T-CWFC模型檢測工具是在Windows 7活動系統(tǒng)平臺，eclipse 4.3.2、 java jdk 1.7和JFLAP 7.0環(huán)境下開發(fā)。本節(jié)以文獻(xiàn)[6]中所給出的通信構(gòu)件Comp和User的接口自動機(jī)模型對T-CWFC模型檢測工具進(jìn)行應(yīng)用說明。

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

圖4 通信構(gòu)件的IA模型

根據(jù)良構(gòu)性定義5就能從直觀上判斷Comp是良構(gòu)的，而User對外界環(huán)境提供的通信異?；顒訜o響應(yīng)，在外界環(huán)境滿足其輸入假設(shè)時則是良構(gòu)的。運(yùn)行T-CWFC進(jìn)行User和Comp良構(gòu)性檢測的結(jié)果如圖5所示。其中:界面左邊的“JFLAP建模IA”按鈕則是利用有限自動機(jī)建模JFLAP插件用于對接口自動機(jī)進(jìn)行建模;“選擇(IA)jff文件”則是選擇待檢測構(gòu)件的建模文件;“良構(gòu)性檢測”按鈕則是根據(jù)算法1和2檢測所選的jff文件的良構(gòu)性，并在界面的右側(cè)文本區(qū)域顯示出檢測結(jié)果。

圖5 通信構(gòu)件的T-CWFC運(yùn)行界面

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

圖4(b)顯示Comp的IA模型中存在三個環(huán)路，且從狀態(tài)s2和s4到初始狀態(tài)s0均分別有兩個選擇分支，則對Comp對應(yīng)的可達(dá)圖進(jìn)行DFS遍歷時共有四條簡單有序集。圖5(b)顯示運(yùn)行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遍歷可得到的。對于構(gòu)件Comp中提供的方法活動msg，從圖4(b)可分析出使能其返回活動ok的狀態(tài)為s5，且從s1到s5的最短路徑為(s1,send!m,s2)→(s2,ack?r,s5)。圖5(b)的結(jié)果顯示，方法活動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)，該有序集所包含的遷移中存在具有相同起始狀態(tài)的遷移，且其中的部分相鄰的兩個遷移中存在前一個遷移的終止?fàn)顟B(tài)不等于后一個遷移的起始狀態(tài)的情況，即DFS遍歷得到的有序集中存在環(huán)路和不連續(xù)遷移，按2.2節(jié)的最簡路徑化簡方法去除環(huán)路并將不連續(xù)的路徑變成連續(xù)得到的最簡運(yùn)行為(s1,send!m,s2)→(s2,ack?r,s5)，根據(jù)定義4可知，從s1到s5是自治無異?？蛇_(dá)的。

同理，圖5(b)的運(yùn)行結(jié)果顯示：首次調(diào)用方法活動send的終止?fàn)顟B(tài)s2到使能其返回活動的s2的運(yùn)行和化簡后的運(yùn)行、第二次調(diào)用方法活動send的終止?fàn)顟B(tài)s4到使能其返回活動的s4均與實際分析得到的相同，且發(fā)現(xiàn)該兩種方法活動到達(dá)的狀態(tài)與使能其返回活動的狀態(tài)相同，即自治無異常可達(dá)的。

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

4 結(jié)語

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

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ī)——一種用于組件組合的形式系統(tǒng)[J].計算機(jī)科學(xué),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服務(wù)流程相容性和相似性分析[J].計算機(jī)學(xué)報, 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] 雷斌,王林章,卜磊,等.基于狀態(tài)機(jī)模型的構(gòu)件健壯性測試[J].軟件學(xué)報,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] 王文霞.有向圖的同構(gòu)判定算法:出入度序列法[J].山西大同大學(xué)學(xué)報(自然科學(xué)版),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。 基金項目:江蘇省產(chǎn)學(xué)研項目(BY2013015- 40)。

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

1001- 9081(2017)02- 0574- 07

10.11772/j.issn.1001- 9081.2017.02.0574

TP311

A