李 雪，朱嘉鋼

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

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

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

李 雪*，朱嘉鋼

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

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

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

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

0 引言

在軟件開發(fā)過程中，基于構(gòu)件的設(shè)計(jì)已成為處理復(fù)雜系統(tǒng)、提高生產(chǎn)力和產(chǎn)品質(zhì)量的一個(gè)重要途徑。構(gòu)件封裝特定功能，并通過接口(interface)來與構(gòu)件式系統(tǒng)中的其他構(gòu)件實(shí)現(xiàn)通信。在構(gòu)建構(gòu)件式系統(tǒng)時(shí)，對(duì)參與組合的構(gòu)件的功能性和非功能性進(jìn)行分析檢測(cè)，是提高系統(tǒng)可靠性的有效途徑之一。在檢測(cè)已發(fā)現(xiàn)構(gòu)件、重構(gòu)的構(gòu)件的良構(gòu)性時(shí)，若發(fā)現(xiàn)其為非良構(gòu)的，則必須拒絕其參與系統(tǒng)的構(gòu)造[1]。為此，在組合構(gòu)件系統(tǒng)、替換或細(xì)化現(xiàn)有構(gòu)件式系統(tǒng)中的某個(gè)構(gòu)件時(shí)，為使替換后系統(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)境時(shí)，即構(gòu)件接口在其某個(gè)內(nèi)部狀態(tài)上不能接受某個(gè)輸入時(shí)，外界環(huán)境不為其提供該輸入[2]。該思想認(rèn)為接口自動(dòng)機(jī)(Interface Automaton, IA)是否是良構(gòu)的，取決于是否存在一個(gè)合適的環(huán)境能夠滿足構(gòu)件接口的所有輸入假設(shè)而使非法狀態(tài)不會(huì)達(dá)到，而未考慮在外界環(huán)境滿足其輸入假設(shè)時(shí)，接口自身內(nèi)部的良構(gòu)性。文獻(xiàn)[3]采用著色Petri網(wǎng)對(duì)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]通過為接口自動(dòng)機(jī)中每個(gè)狀態(tài)添加時(shí)鐘變量實(shí)現(xiàn)對(duì)具有實(shí)時(shí)特性的構(gòu)件進(jìn)行建模，并在文獻(xiàn)[6]中提出的良構(gòu)性基礎(chǔ)上增加了時(shí)間良構(gòu)性約束條件。文獻(xiàn)[7]則通過擴(kuò)大接口自動(dòng)機(jī)中自治活動(dòng)的范圍，在考慮外界環(huán)境滿足構(gòu)件需求的情況下，給出了接口自動(dòng)機(jī)良構(gòu)性的定義，即其與環(huán)境交互時(shí)接口內(nèi)部自身能夠正確運(yùn)行而不會(huì)一直停留在某一狀態(tài)，并指出當(dāng)參與組合的接口自動(dòng)機(jī)是良構(gòu)的且其語義兼容時(shí)，則其組合系統(tǒng)也是良構(gòu)的。但是，這些研究均未給出構(gòu)件良構(gòu)性的具體檢測(cè)算法，只能由開發(fā)者自行根據(jù)定義描述來判定，降低了開發(fā)效率。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1)

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

2)

vt1?v0∈V′;

//取出第一個(gè)頂點(diǎn)

3)

4)

vt1?v′i，轉(zhuǎn)3)；

5)

結(jié)束。

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

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

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

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

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

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

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

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

1)

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

2)

檢測(cè)每個(gè)mi到對(duì)應(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)

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

i)

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

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

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

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

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

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

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

3.1.1IA模型輸入處理

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

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

圖2 簡(jiǎn)單有序集獲取的流程

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

3.1.3 良構(gòu)性檢測(cè)

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

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

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

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

3.2 應(yīng)用實(shí)例

本文設(shè)計(jì)和實(shí)現(xiàn)的T-CWFC模型檢測(cè)工具是在Windows 7活動(dòng)系統(tǒng)平臺(tái)，eclipse 4.3.2、 java jdk 1.7和JFLAP 7.0環(huán)境下開發(fā)。本節(jié)以文獻(xiàn)[6]中所給出的通信構(gòu)件Comp和User的接口自動(dòng)機(jī)模型對(duì)T-CWFC模型檢測(cè)工具進(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方法活動(dòng)，且在該方法活動(dòng)被調(diào)用時(shí)給出相應(yīng)的返回活動(dòng)ack和異?；顒?dòng)nack，所以當(dāng)Comp中方法活動(dòng)msg被外部調(diào)用時(shí)，構(gòu)件將先調(diào)用send方法活動(dòng)與其環(huán)境進(jìn)行交互，并在接收環(huán)境提供的返回活動(dòng)ack之后，向調(diào)用者返回通信成功信息ok；若連續(xù)兩次send請(qǐng)求活動(dòng)接收到的都是一次活動(dòng)nack，則向通信者返回通信異常fail。圖4(b)的IA模型描述了構(gòu)件Comp的使用者構(gòu)件User在假設(shè)環(huán)境確定下的行為特征，其對(duì)環(huán)境的假設(shè)為當(dāng)其調(diào)用環(huán)境Comp提供的msg消息時(shí)，則會(huì)得到通信成功ok信息和通信異常fail信息。

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

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

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

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

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

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

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

4 結(jié)語

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

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] 張巖,胡軍,于笑豐,等.接口自動(dòng)機(jī)——一種用于組件組合的形式系統(tǒng)[J].計(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ì)算機(jī)學(xué)報(bào), 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)件健壯性測(cè)試[J].軟件學(xué)報(bào),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é)報(bào)(自然科學(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。 基金項(xiàng)目:江蘇省產(chǎn)學(xué)研項(xiàng)目(BY2013015- 40)。

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

1001- 9081(2017)02- 0574- 07

10.11772/j.issn.1001- 9081.2017.02.0574

TP311

A