基于ＥＦＳＭ用戶自定義故障模型的測試集生成

摘 要:提出了一種用戶自定義故障的EFSM測試集生成方法。該方法應用EFSM切片對EFSM模型進行合理的縮減，有效地避免了從EFSM到FSM轉換得到測試集而產生狀態空間爆炸的問題，也得到最短的測試用例集合。實驗結果表明了新算法對生成最短EFSM測試集是有效的。

關鍵詞:擴展有限狀態機(EFSM); 用戶自定義故障; 一致性測試; 測試生成

中圖分類號:TP311文獻標志碼:A

文章編號:1001-3695(2009)09-3388-04

doi:10.3969/j.issn.1001-3695.2009.09.053

Method for generating test suite based on user-defined faults in EFSM model

LI Yong-liang， LI Rui， LI Ren-fa， ZHANG Yan

(School of Computer Communication， Hunan University， Changsha 410082， China)

Abstract:This paper presented a method for test generation based on user-defined faults for EFSM specifications. The algorithm used appropriate slices of the specification EFSM in order to avoid state space explosion when converting EFSM model to FSM model， these slices were much smaller than the given specification， meanwhile got the shortest test suite. Finally， the article gave a simple protocol to be verified. The experiment proves that the algorithm is effective to generate shortest EFSM test suite.

Key words:extended finite state machine; user-defined faults; conformance testing; test generation

0 引言

在基于FSM[1，2]的測試生成中，提出了用戶定義故障和給定故障類型的測試生成方法，主要是為了減少一致性測試開銷(測試套的長度)，這種方法僅適用于給定FSM故障類型的情形。以上方法在基于FSM的增量測試模型[3]中得到擴展，根據修改后的規約模型生成被修改規約的部分測試用例。以上方法[1~3]都產生大量不必要的測試用例，效率比較低。EFSM模型是在FSM中引入了輸入和輸出參數、前置條件、上下文變量，定義在上下文變量和輸入參數上的操作。EFSM規約模型一致性測試的問題主要包括消除EFSM規約模型的不可執行路徑和測試集生成[4~6]等問題。在基于EFSM模型的故障診斷[7]中，通過將給定EFSM故障模型展開成與之等價的FSM模型生成故障診斷用例，很明顯展開的系統狀態數量急劇擴大，容易產生狀態空間爆炸的問題。因此，FSM一致性測試生成方法就不能簡單地應用到EFSM模型中。

本文擴展了關于系統規約和被測系統都是采用EFSM規約來表示、用戶定義故障[8]的測試集生成的研究。從給定EFSM規約中選擇可疑變遷集合，為了減少測試生成的開銷，沒有直接地把EFSM故障模型展開成相應的FSM故障模型，而是對EFSM 模型規約切片(縮減)，生成用戶自定義故障的完備測試套。該方法通過切片EFSM規約模型后，得到保持完備測試推導特性的更小的狀態機。一方面，提出的切片算法保持著遍歷可疑變遷和區分變遷終止狀態的原有特性;另一方面，切片后的模型遠遠小于給定的EFSM規約模型，以此來提高測試開銷。

1 EFSM模型規約及定義

1.1 EFSM規約模型

一個擴展有限狀態機(EFSM)[5]是一個(S， T)狀態變遷對，其中S是狀態的集合，T是狀態間變遷的集合。每個變遷t∈T是七元組(s，i，P，op，o，up，s′)，其中:

s，s′∈S是初始狀態和終結狀態;

i∈I是輸入，I是輸入的集合，Di是輸入向量的集合，一個輸入向量的每個元素對應于與i相關的一個輸入參數;

o∈O是輸出，O是輸出的集合，Do是輸出向量的集合，一個輸出向量的每個元素對應于與o相關的一個輸出參數;

P，op 和 up是定義在輸入參數和上下文變量V 上的函數;

P:Di×Dv→{true，1}是謂詞， Dv是上下文變量V 的集合;

op:Di×Dv→Do是一個輸出參數函數;

up:Di×Dv→Dv是一個上下文修改函數。

EFSM的狀態格局表示為狀態s和上下文變量v的組合(s，v)。在本文中討論EFSM模型是已經給出了初始狀態和格局的規約模型，并且引入一個全局的重置r操作，該操作可以回到初始狀態格局;再給定一個EFSM參數化的輸入序列和狀態格局，就可以通過輸入序列模擬EFSM的行為計算對應的輸出序列。

1.2 EFSM 中的定義

設t是一個變遷，use(t)是在變遷t 中引用的變量集合，包括謂詞(前置條件)和行為(賦值)以及輸出;def(t)是在變遷t中定義的變量集合，包括行為和輸入。I_use(t)表示變遷t中輸入變量引用集合，P_use(t)表示變遷t中謂詞(前置條件)引用的變量集合，O_use(t)表示在變遷t中輸出引用的變量集合，C_use(t)表示變遷t中更新和賦值涉及到上下文變量集合。

定義1 依賴關系。反映了變遷間通過變量賦值影響的關系。如果存在一個變量v，且v∈def(ti)，v∈use(tj)，在EFSM中存在一條從ti到tj的路徑(變遷序列)，在該路徑上變量v不被重定義，則稱變遷ti和tj之間存在依賴關系。

定義2 區分序列。當EFSM模型ES和EF在相同的輸入條件下，輸入參數化序列α，對應于ES、EF中相同的輸出，則這兩個EFSM模型ES和EF是一致的。如果存在一個參數化序列α，在EF和ES中對應的輸出不相同，則EF和ES是可區分的，可以寫成EFαES或簡單地寫成EFES。

圖1給出了一個EFSM規約形式的簡圖。它有四個狀態，兩個參數化的輸入a(x)和b(y)，一個非參數化的輸入c，兩個參數化的輸出O(z)和F(w)，兩個非參數化的輸出R和NULL，還有兩個上下文變量v和w。這個初始格局包括狀態s1及上下文變量v=0和w=0，則可以寫成(s1，(0，0))。

假設本文中EFSM規約和被測系統都是一致的、確定的和完整的[5]。EFSM都是定義在參數化輸入上的，對于每個參數化的輸入序列和狀態格局，在EFSM模型中對應惟一的輸出序列。

2 故障模型

2.1 EFSM故障模型

在EFSM一致性測試中，故障模型(ES，～，E)是測試生成的基礎，建立的故障模型包括給定系統的EFSM規約ES，被測系統中所有可能的故障集合即故障域E，還包括系統規約和故障域之間的一致性關系～。假設故障域E的行為是定義在參數化的輸入序列下的，若在EFSM規約模型與EFSM被測系統一致性關系～被滿足，則這個被測系統是一致的系統執行;否則這個被測系統是不一致的。本文中考慮的是EFSM模型的等價關系。若被測系統EI≌ES，那么被測系統EI(EI∈E)就是與系統規約相一致;否則與系統規約不一致。

假設建立的EFSM故障模型只包括輸出和轉移故障，EFSM被測系統EI中的變遷t=(s，x，P，op，y，up，s′)。如果變遷t的輸出與EFSM規約模型中的輸出結果不相同，那么就說被測系統EI中的變遷t存在著輸出類型的故障;當變遷t的最終狀態與EFSM規約模型中對應變遷的最終狀態不相同時，那么這個變遷t存在著轉移故障。在EFSM被測系統中變遷t的輸出和終止狀態與EFSM規約模型中不同時，則變遷t就存在著輸出和轉移的故障。

2.2 故障模型的建立

給定EFSM規約模型ES，對于ES中所有的可疑變遷t，在ES中添加這些可疑變遷對應的輸出和轉移故障的變遷，并且包括相同的輸入和上下文變量，最后得到被測系統模型EMM-trans-out。例如對于一個可疑變遷t′=(s，x，P，op，y，up，s′)，若y′≠y，將變遷t=(s，x，P，op，y′，up，s′)添加到ES模型中;若s″≠s′，把變遷對應的輸出轉移故障變遷t″=(s，x，P，op，y′，up，s″)添加到ES模型中。最后得到擴展有限狀態機EMM-trans-out是一個完全的，但常常是不確定的，ES則為它的一個子狀態機。如果只需要檢測可疑轉移中的輸出故障，對應的EMM-out擴展有限狀態機只需要在ES中添加所有可能發生輸出故障的變遷，步驟同EMM-trans-out的過程。

3 EFSM切片算法

3.1 切片算法

基于狀態遷移系統的切片[5]中，當得到完全的輸出和轉移故障的測試用例，通常不得不遍歷EFSM規約中合適的轉移和區分變遷t的最終狀態s′與其他狀態s″，即s≠s′。因為EFSM模型中又增加了上下文變量，本文提出了保留與原有EFSM同樣的遍歷和區分狀態的EFSM規約的切片算法。

算法1 對EFSM模型上下文變量的切片

輸入:EFSM模型ES，上下文變量集合為V;

輸出:與ES具有相同的變遷執行功能的縮減SliceT(ES)模型。

首先初始化變量集合Vd，對EFSM模型ES中的每一條變遷:

a)若v=P_use(t)∈V，則把變量v放入變量集合Vd中，獲得的變量集合VdV。

b)若v=C_use(t)∈Vd，則刪除這條變遷上的賦值op以及更新up操作。

c)若v=O_use(t)∈Vd，則給輸出參數賦一個Do集合內的一個數值，若輸出為參數化輸出，則計算一個參數區間的值賦給輸出。SliceT(ES)表示切片縮減到EFSM。結束算法1。

給定EFSM模型ES，SliceT(ES)表示給定ES通過算法1得到的切片模型。如果參數化輸入序列α可以從sliceT(ES)的初始狀態到達s狀態。而且如果這個參數化的序列α可以從ES的初始狀態到達s狀態，那么α也可以從縮減的sliceT(ES)的初始狀態到達s狀態。也就是說如果變遷t=(s，x，P，op，y′，up，s′)在sliceT(ES)中可以通過α序列被執行，那么在ES中相同的變遷通過α也會被執行。

對于圖1所示的EFSM規約模型ES0，上下文變量w沒有影響ES0的前置條件謂詞。因此，t5的w:=0，刪除變遷t10的賦值操作w:=w+1，和t11的w:=w-1，再把變遷t5，t10，t11對參數w的輸出操作F(w)賦值為0，得到sliceT(ES0)。

為了簡化生成輸入序列的過程需要遍歷合適的變遷和區分終止狀態，另一個切片sliceFSM(ES)是獨立于上下文變量值的行為。

算法2 生成一個具有FSM行為的切片模型

輸入:EFSM模型ES，上下文變量集合為V;

輸出:sliceFSM(ES)。

a)對EFSM模型ES中的每一條變遷，若v=P_use(t)∈V，即EFSM模型中的變遷t的前置謂詞依賴于上下文變量集合中變量v，那么刪除該條變遷。

b)對ES中剩下的每條變遷t=(s，x，P，op，y′，up，s′)，若變遷t依賴于輸入參數，那么用變遷(s，x，y′，s′)替換ES中的變遷t，其中x為參數化的輸入，并且使得前置謂詞P為true，得到sliceFSM(ES)，在這里不考慮參數化的輸出，y′是一個表示輸出符號。算法2結束。

通過算法2對圖1的EFSM模型ES0生成切片模型。首先按算法第a)步刪除ES0中的變遷t3，t8，t10，然后執行算法第b)步替換ES0中的變遷，得到圖2所示的sliceFSM(ES0)。

3.2 測試生成充分條件

在測試序列生成的研究中，提出很多消除EFSM中狀態可執行性的方法[4，6]。在本文中為了簡化問題，在后面的測試生成中提出以下幾個假設條件:

條件1 給定EFSM模型ES和模型中可疑變遷集合，對于每一個可疑轉移t=(s，x，P，op，y′，up，s′)，存在著一個參數化的序列α，使得變遷t的前置條件P為真，參數化序列能夠從ES的初始狀態格局到達〈s，v〉。如果EFSM被測系統EI與規約模型ES輸出不同，那么ES和EI就可以通過可疑轉移上的參數化輸入序列來區分。

條件2 給定ES中的變遷t=(s，x，P，op，y′，up，s′)和一個從sliceFSM(ES)的初始狀態到達狀態s得到的參數化的序列α，其中變遷t中的P不依賴于上下文變量，那么ES模型中的變遷t可以通過序列αx遍歷從ES的初始狀態到達狀態s(x是定義在sliceFSM(ES)狀態s的參數化的輸入向量)。

條件3 給定兩個狀態s和s′分別為EFSM模型ES與sliceFSM(ES)中的狀態，如果這兩個狀態可以通過sliceFSM(ES)中的輸入序列α區分，那么每兩個狀態格局(s，v)和(s′，v′)可以從ES的初始格局通過序列α到達。

4 測試生成

4.1 輸出故障的測試生成

本文提出了測試在可疑變遷中輸出故障的測試生成算法。給定EFSM規約模型ES和ES中可疑變遷集合。根據上文給出的充分條件，sliceT(ES)和sliceFSM(ES)保持了EFSM模型ES的遍歷能力，所以這兩個切片算法都應用到驗證可疑變遷輸出錯誤的測試生成過程中。

算法3 驗證可疑變遷輸出錯誤的測試生成

輸入:EFSM規約ES和ES的可疑變遷集合;

輸出:驗證故障模型〈ES，≌，sub(EMM-out)〉可疑變遷中的輸出故障的完全測試套TS。

a)初始化TS=，獲得在ES中所有的可疑變遷的輸出故障集合PFo。得到集合PFo的過程為:如果變遷t=(s，x，P，op，y′，up，s′)是可疑變遷，那么把變遷t加入到集合PFo。根據算法2得到EFSM模型ES的sliceFSM(ES)模型。

b)對可疑變遷集合PFo中的每一個變遷t=(s，x，P，op，y′，up，s′)，假設每個變遷的長度為1，然后根據變遷中的輸入構造sliceFSM(ES)模型到可疑變遷的最短(構造一個由初始狀態到可疑變遷終止狀態的最短的生成樹)參數化序列α，選擇從sliceFSM(ES)的初始狀態到達狀態s的參數化序列α，和變遷中已經定義的參數化輸入x，那么序列αx就是一條驗證可以變遷t的一條最短的測試序列，把序列αx添加到測試套TS中并且移除可疑變遷集合PFo中的變遷t。如果集合PFo=，算法3結束。

c)通過算法1得到ES的切片模型sliceT(ES)。對集合中剩下的每一個變遷t∈PFo，同樣按步驟a)中的方法生成最短參數化的輸入序列α，序列α從sliceT(ES)的初始狀態格局遍歷變遷t，把序列α添加到測試套TS中。算法3結束。

在算法3中通過算法1和2的切片算法，可以避免EFSM到FSM的展開而導致狀態空間爆炸的問題，得到了遍歷可疑變遷的輸出故障的測試序列集合TS。但是由于在轉移和輸出故障的驗證中需要區分變遷的終止狀態，所以生成的測試序列集合就不能驗證EFSM輸出和轉移類型的故障。

4.2 轉移和輸出故障的測試生成

算法4 驗證可疑變遷轉移和輸出故障的測試生成

輸入:EFSM規約ES和ES的可疑變遷集合;

輸出:驗證故障模型〈ES，≌，sub(EMM-trans-out)〉可疑變遷中的輸出故障的完全測試套TS。

a)初始化TS=，如果變遷t=(s，x，P，op，y′，up，s′)是存在輸出和轉移故障的可疑變遷，那么把所有的變遷(s，x，P，op，y′，up，s″)添加到可疑變遷集合PFtro(s″≠s′)，最終得到集合PFtro。通過算法2得到EFSM模型ES的sliceFSM(ES)切片模型，并在sliceFSM(ES)中標記對應ES中的可疑變遷。

b)如果在sliceFSM(ES)中不存在可疑的變遷通過非可疑變遷到達，那么轉c);否則，對sliceFSM(ES)中的每一個可疑變遷t=(s，x，y，sj)通過遍歷非可疑變遷用參數化的序列α:

(a)對每一個可疑變遷(s，x，P，op，y′，up，sk)∈PFtro，其中的sk≠sj。檢測sliceFSM(ES)，如果狀態sk和sj可以通過序列β區分，并且區分序列β通過遍歷sliceFSM(ES)中的可疑變遷得到，那么把序列αxβ添加到TS集合，刪除PFtro集合中的變遷(s，x，P，op，y′，up，sk)。

(b)如果對每一個變遷中的狀態sk≠sj，集合PFtro中沒有變遷(s，x，P，op，y′，up，sk)，那么在ES和sliceFSM(ES)中標記變遷t為非可疑變遷，轉b)。

c)如果可疑變遷集合PFtro為空，那么算法4結束;否則，根據文獻[5]獲得區分可疑變遷中最終狀態的序列α，把序列α添加到TS中，并標記此變遷為非可疑變遷，從集合PFtro刪除變遷。若PFtro仍不為空，轉d)。

d)通過算法1得到ES的切片模型sliceT(ES)。對集合中剩下的每一個變遷t∈PFtro，標記得到的切片模型中的可疑變遷，同樣按算法3中的方法生成最短參數化的輸入序列α ，序列α從sliceT(ES)的初始狀態格局遍歷變遷t，把序列α添加到測試套TS中。算法4結束。

5 實驗分析

下面以簡化的Initiator-Responder[9]協議為例進行實驗驗證，圖3為Initiator-Responder協議的EFSM模型，表示為ESIR。該協議中EFSM模型初始狀態為disconnect，有4個狀態和15條變遷轉移;該協議模型部分展開后得到9個狀態和29條變遷[4]，部分展開的模型應用HIS[10]測試生成方法獲得的完全測試套的長度為462。

為了得到ESIR在選擇可疑變遷輸出(輸出和轉移)故障的完全測試套，首先選擇ESIR的每一條變遷，并標記變遷為可疑變遷。應用本文中的方法得到所有可疑變遷中每個變遷的輸出(輸出和轉移)變遷故障的完全測試套的總長度為47(62)，測試用例平均長度為3.1(4.1)。

6 結束語

本文提出一種基于EFSM切片的用戶自定義故障模型的測試生成方法，該測試生成方法適用于由用戶自定義的故障模型選擇需要測試的變遷，或是由于系統規約被修改而需要重新生成測試集的情況。新方法與以往基于EFSM故障模型狀態驗證序列生成算法相比具有兩大優點:a)該方法對EFSM規約模型進行切片，不需要將EFSM模型轉換成相應的FSM模型;b)建立的EFSM故障模型可以根據用戶自定義故障類型生成最短的測試套。

參考文獻:

[1]KOUFAREVA I， PETRENKO A， YEVTUSHENKO N. Test generation driven by user-defined fault models[C]//Proc of the 12th International Workshop on Testing Communicating Systems. 1999:215-236.

[2]PETRENKO A， YEVTUSHENKO N. Test suite generation for a FSM with a given type of implementation errors[C]//Proc of the 12th Symposium on Protocol Specification， Testing Verification. 1992:229-243.

[3]EL-FAKIH K， YEVTUSHENKO N， BOCHMANN G. FSM-based incremental testing methods[J]. IEEE Trans on Software Enginee-ring， 2004， 30(7):425-436.

[4]HIERONS R， KIM T， URAL H. Expanding an extended fnite state machine to aid testability[C]//Proc of COMPSAC. 2002:334-242.

[5]PETRENKO A， BORODAY S， GROZ R. Confirming configurations in EFSM testing[J]. IEEE Trans on Software Engineering， 2004， 30(1):29-42.

[6]舒挺，魏仰蘇，吳柏青，等. EFSM可執行狀態驗證序列的生成[J].北京郵電大學學報，2007，30(2):84-88.

[7]EL-FAKIH K， PETRENKO S， YEVTUSHENKO N， et al. Fault dia-gnosis in extended finite state machines[C]//Proc of TestCom. Berlin:Springer， 2003:197-210.

[8]EL-FAKIH K，KOLOMEEZ A， PROKOPENKO S， et al. Extended finite state machine based test derivation driven by user defined faults[C]//Proc of International Conference on Software Testing， Verification， and Validation. Washington DC:IEEE Computer Society， 2008:308-317.

[9]HUANG Chug-ming， CHIANG Meng-shu， JANG Ming， et al. UIOE:a protocol test sequence generation method using the transition executability analysis (TEA)[J]. Computer Communication， 1998，21(16):1462-1475.

[10]PETRENKO A， YEVTUSHENKO N. Testing from partialdeterministic FSM specifications[J]. IEEE Trans on Computers， 2005， 54(9):1154-1165.