龍慶　王璠

摘要：為了達(dá)到運用切片技術(shù)對構(gòu)件模型進(jìn)行狀態(tài)空間壓縮的目的，在構(gòu)件之間接口的交互關(guān)系的基礎(chǔ)上，提出了用測試驅(qū)動節(jié)點和擴(kuò)展的構(gòu)件節(jié)點建立構(gòu)件系統(tǒng)的功能依賴圖的具體方法和步驟，并通過基于模型檢驗的接口變異測試方法對三角形問題的JavaBean構(gòu)件在切片前后的模型分別進(jìn)行了測試。實驗結(jié)果表明，該方法能夠有效地壓縮系統(tǒng)的狀態(tài)空間，提高測試效率，同時也保證了對構(gòu)件接口測試的全面性和正確性。

關(guān)鍵詞： 模型檢驗；接口變異；切片技術(shù)；功能依賴圖

中圖分類號：TP311 文獻(xiàn)標(biāo)識碼：A 文章編號：1009-3044（2015）02-0211-04

Abstract：Motivated by compressing the model of component through slicing technique， this paper employs the interactive relationship of the components. Then it proposes a method of constructing a function dependence graph for component system， which is made of a test driver node and some extended component nodes. Finally， by an example， it demonstrates that this method could not only decrease the size of the state space and increase the efficiency for testing generation， but also guarantee the comprehension and the validity of the interface testing for JavaBean components while applying the method of interface mutation testing based on model checking.

Key words： model checking； interface mutation； slicing technique； function dependence graph

模型檢驗技術(shù)作為一種形式化驗證方法，以其自動化程度高的特點已經(jīng)廣泛應(yīng)用于計算機(jī)硬件、通信協(xié)議的分析與驗證等許多領(lǐng)域，它通過窮盡地搜索有限狀態(tài)系統(tǒng)的狀態(tài)空間，從而判定系統(tǒng)（模型）的每一個狀態(tài)是否滿足給定的性質(zhì)，并且總會以“是”或“否”為結(jié)果而終止[1]。目前，利用模型檢驗技術(shù)進(jìn)行測試用例生成的研究也十分活躍，并且也取得了一定的研究成果[2]。同時，隨著程序模型檢驗工具的誕生，一些將變異測試方法與程序模型檢驗工具相結(jié)合并生成測試用例的研究工作也得到了一定進(jìn)展[3]。

盡管模型檢驗技術(shù)在自動化方面具有許多優(yōu)點，但它是采用窮盡搜索系統(tǒng)空間的方法對所給定的性質(zhì)進(jìn)行驗證，因此，對并發(fā)系統(tǒng)而言，其狀態(tài)數(shù)往往隨并發(fā)分量的增加呈指數(shù)增長，這樣就產(chǎn)生了“狀態(tài)空間爆炸”（state-explosion）問題[1]。對于基于模型檢驗的變異測試來說，當(dāng)對非等價變異體采用“搜索所有的反例路徑”的策略進(jìn)行驗證，以及對等價變異體進(jìn)行驗證時，都必須通過搜索整個系統(tǒng)的狀態(tài)空間才能夠進(jìn)行判定，所以這樣就影響了模型檢驗的驗證效率。

因此，為了壓縮系統(tǒng)狀態(tài)空間的數(shù)量，本文將通過建立構(gòu)件系統(tǒng)的功能依賴圖，然后運用切片技術(shù)[4]對其進(jìn)行切片。最后，本文將以Java PathFinder作為模型檢驗工具，采用基于模型檢驗技術(shù)的接口變異測試方法[5]對JavaBean構(gòu)件進(jìn)行接口變異測試，并對所切片效果進(jìn)行驗證。圖1給出了該方法的測試用例生成框架。

1 構(gòu)件系統(tǒng)的功能依賴圖

S.Horwitz等人通過引入系統(tǒng)依賴圖（System Dependence Graph，SDG）的概念表示了具有多個過程的程序依賴圖[6]，但是使用該方法就必須知道每一個過程內(nèi)部的具體細(xì)節(jié)信息，因此這種方法并不適用于在源碼未知情況下的構(gòu)件化軟件切片；雖然文獻(xiàn)[7]提出了一種能夠?qū)τ蓸?gòu)件所組成的系統(tǒng)進(jìn)行切片的方法，但是這種方法卻只考慮了構(gòu)件之間接口的交互關(guān)系而忽略了構(gòu)件在系統(tǒng)中的狀態(tài)。因此，本文以文獻(xiàn)[8]所提出的構(gòu)件之間接口的交互關(guān)系為基礎(chǔ)，在細(xì)化了構(gòu)件之間的接口交互圖后，使其能夠在清晰描述源碼未知情況下被測試構(gòu)件的狀態(tài)和接口函數(shù)之間的關(guān)系的同時，也能夠使切片技術(shù)適用于對被測試構(gòu)件系統(tǒng)的接口調(diào)用關(guān)系模型的狀態(tài)空間的壓縮。

1.1 功能依賴圖的組成

本文以該被測試構(gòu)件的接口規(guī)約說明為依據(jù)，通過測試驅(qū)動程序?qū)Ρ粶y試構(gòu)件，或者是將該被測試構(gòu)件和與之相關(guān)的構(gòu)件關(guān)聯(lián)后進(jìn)行建模，從而建立被測試構(gòu)件的接口調(diào)用關(guān)系模型。通過這個構(gòu)件系統(tǒng)的接口調(diào)用關(guān)系模型，被測試構(gòu)件所具備的相關(guān)功能會在利用模型檢驗技術(shù)進(jìn)行驗證的過程中表現(xiàn)出來。因此，將細(xì)化后的構(gòu)件之間的接口交互關(guān)系稱之為構(gòu)件系統(tǒng)的功能依賴圖（Function Dependence Graph，F(xiàn)DG），并且該圖是由測試驅(qū)動節(jié)點（Test Driver Node）和構(gòu)件節(jié)點（Component Node）兩種類型的節(jié)點所組成。

測試驅(qū)動節(jié)點是由被測試構(gòu)件的測試驅(qū)動程序所虛擬出來的一個節(jié)點，它是整個構(gòu)件系統(tǒng)的主體框架。從切片技術(shù)的觀點來分析，該節(jié)點實際上就是它所代表的測試驅(qū)動程序的過程依賴圖[3]（Process Dependence Graph）。

構(gòu)件節(jié)點實際上在代表被測試構(gòu)件的同時，也可以代表與被測試構(gòu)件相關(guān)聯(lián)的構(gòu)件。為了能夠應(yīng)用切片技術(shù)對其進(jìn)行切片，需要通過添加一些輔助接點對構(gòu)件節(jié)點及輔助邊對其進(jìn)行細(xì)化。這里通過定義一個五元組C = 來描述一個構(gòu)件節(jié)點，具體如圖2所示。

1） 構(gòu)造函數(shù)輔助節(jié)點（Construction Assistant Node）的集合Con

對于JavaBean構(gòu)件來說，為了體現(xiàn)面向?qū)ο蟮奶卣鳎跇?gòu)件節(jié)點中應(yīng)該添加與之相關(guān)的所有構(gòu)造函數(shù)的構(gòu)造函數(shù)輔助節(jié)點（Conk表示構(gòu)件中第k個構(gòu)造函數(shù)）。輔助節(jié)點實際上就是該構(gòu)件的入口節(jié)點。

2） 狀態(tài)輔助節(jié)點（State Assistant Node）的集合S

由于在代碼未知情況下的構(gòu)件接口測試是一種黑盒測試，因此，還必須在構(gòu)件節(jié)點中添加表示構(gòu)件狀態(tài)的狀態(tài)輔助節(jié)點（Si表示構(gòu)件中第i個狀態(tài)）。

3） 接口函數(shù)輔助節(jié)點（Interface Function Assistant Node）的集合I

在構(gòu)件節(jié)點中添加表示該構(gòu)件所包含的所有接口函數(shù)的接口函數(shù)輔助節(jié)點（Im表示構(gòu)件中第m個接口函數(shù)）。

4） 輸入?yún)?shù)輔助節(jié)點（Input Parameter Assistant Node）的集合p

對于每一個包含輸入?yún)?shù)的接口函數(shù)應(yīng)該在其所對應(yīng)的接口函數(shù)輔助節(jié)點中添加表示該接口函數(shù)中所有參數(shù)的輸入?yún)?shù)輔助節(jié)點（pn表示該接口函數(shù)中的第n個參數(shù)）。

5） 輔助節(jié)點之間輔助邊（Assistant Edge）的集合E

為了能夠體現(xiàn)出上述輔助節(jié)點之間的內(nèi)在關(guān)系并使切片技術(shù)能夠適用于構(gòu)件節(jié)點，還必須根據(jù)構(gòu)件的規(guī)約說明在輔助接點之間添加相應(yīng)的邊。首先，由于通過構(gòu)造函數(shù)在實例化一個構(gòu)件的時候，與該構(gòu)件相關(guān)的狀態(tài)和接口調(diào)用函數(shù)也會被創(chuàng)建，因此，就必須在構(gòu)造函數(shù)輔助節(jié)點和狀態(tài)輔助節(jié)點以及構(gòu)造函數(shù)輔助節(jié)點和接口函數(shù)輔助節(jié)點之間添加一條控制依賴邊；其次，根據(jù)構(gòu)件的接口規(guī)約說明，應(yīng)該在具有控制依賴關(guān)系的接口函數(shù)之間添加能夠代表它們之間控制依賴關(guān)系的控制依賴邊；最后，由于構(gòu)件相關(guān)的狀態(tài)信息是通過與之相關(guān)的構(gòu)件接口函數(shù)進(jìn)行改變的，所以需要在接口函數(shù)輔助節(jié)點和狀態(tài)輔助節(jié)點之間添加一條控制依賴邊，同時，構(gòu)件的狀態(tài)信息也需要通過接口函數(shù)向外界進(jìn)行表現(xiàn)，因此，還應(yīng)該在狀態(tài)輔助節(jié)點和與之相關(guān)接口函數(shù)輔助節(jié)點之間添加一條數(shù)據(jù)依賴邊。綜上所述，構(gòu)件節(jié)點之間輔助邊的集合E是控制依賴邊Ec和數(shù)據(jù)依賴邊Ed的并集，即：E = Ec U Ed。

1.2 功能依賴圖的建立及其切片

在明確了構(gòu)件系統(tǒng)的功能依賴圖的組成后，就應(yīng)該根據(jù)測試驅(qū)動程序?qū)y試驅(qū)動節(jié)點和構(gòu)件節(jié)點進(jìn)行關(guān)聯(lián)，從而建立整個構(gòu)件系統(tǒng)的功能依賴圖，它主要包括建立測試驅(qū)動程序的過程依賴圖和確立該過程依賴圖與構(gòu)件節(jié)點之間關(guān)聯(lián)關(guān)系兩個主要步驟。

文獻(xiàn)[9]給出了建立測試驅(qū)動程序過程依賴圖的具體方法和步驟，故本文在此不作熬述。

本文的研究重點在于對構(gòu)件的接口進(jìn)行測試，因此，對被測試構(gòu)件系統(tǒng)的功能依賴圖的建立主要就體現(xiàn)在確立測試驅(qū)動程序的過程依賴圖和構(gòu)件節(jié)點之間的關(guān)系之上，這些關(guān)系主要包括了如下四個方面：

1） 測試驅(qū)動程序?qū)?gòu)件的實例化

在測試驅(qū)動程序中需要通過構(gòu)造函數(shù)對JavaBean構(gòu)件進(jìn)行實例化。這樣，就必須添加一條描述測試驅(qū)動程序?qū)?gòu)件進(jìn)行實例化的控制依賴邊。

2） 測試驅(qū)動程序?qū)?gòu)件中接口函數(shù)的調(diào)用

對構(gòu)件中接口函數(shù)的每一次調(diào)用，需要添加一條描述測試驅(qū)動程序?qū)涌诤瘮?shù)進(jìn)行調(diào)用的接口函數(shù)調(diào)用邊。

3） 測試驅(qū)動程序?qū)?gòu)件中接口函數(shù)的參數(shù)輸入

對于擁有輸入?yún)?shù)的接口函數(shù)來說，測試驅(qū)動程序在對其進(jìn)行調(diào)用時，對于每一個輸入?yún)?shù)都需要添加一條描述測試驅(qū)動程序在對其進(jìn)行調(diào)用時的參數(shù)輸入邊。

4） 構(gòu)件中接口函數(shù)對測試驅(qū)動程序的響應(yīng)

對接口函數(shù)的調(diào)用實際上相當(dāng)于對構(gòu)件中相關(guān)功能進(jìn)行了一次使用，因此，構(gòu)件就必須向外界產(chǎn)生這個調(diào)用的一個響應(yīng)，這樣，就必須添加一條描述構(gòu)件中接口函數(shù)響應(yīng)的邊。

本文以三角形問題的JavaBean構(gòu)件為例進(jìn)行研究，表1給出了三角形問題構(gòu)件中的接口函數(shù)及接口函數(shù)所對應(yīng)的狀態(tài)。

在依據(jù)三角形問題構(gòu)件的接口規(guī)約說明建立測試驅(qū)動程序后，圖3給出了其構(gòu)件系統(tǒng)的功能依賴圖。圖中右側(cè)部分是測試驅(qū)動程序節(jié)點，它是由被測試構(gòu)件的測試驅(qū)動程序所建立的過程依賴圖組成的[5]；圖中左側(cè)部分是三角形問題構(gòu)件的構(gòu)件節(jié)點，該節(jié)點中的S1、S2和S3分別代表了構(gòu)件中的三個狀態(tài)：bTriangle、 bRight和tType。由于三個接口函數(shù)的輸入?yún)?shù)都是三個整形變量，因此，為了便于觀察，在具體作圖的過程中將輸入?yún)?shù)a、b、c三個節(jié)點視為一個節(jié)點。

建立構(gòu)件系統(tǒng)的功能依賴圖后，就可以運用切片技術(shù)對其進(jìn)行切片。在基于模型檢驗技術(shù)的變異測試方法的測試用例的生成過程中，是通過引入斷言違背機(jī)制將原有模型和變異模型結(jié)合并對構(gòu)件的狀態(tài)進(jìn)行判定從而誘發(fā)錯誤生成并得到反例路徑。因此，為了能夠找到導(dǎo)致這個斷言違背所產(chǎn)生錯誤的原因，就必須找到在這個斷言違背之前，系統(tǒng)模型中哪些語句或者是哪個謂詞表達(dá)式影響了所關(guān)注的這個斷言違背，并且它們是如何傳播到這個地方。這樣在對功能依賴圖進(jìn)行切片時，就可以采用文獻(xiàn)[6]中所提出的后向切片準(zhǔn)則和兩步圖的可達(dá)性算法對構(gòu)件系統(tǒng)的功能依賴圖進(jìn)行切片。

2 實驗結(jié)果和分析

2.1 實驗對象說明及實驗結(jié)果

本節(jié)以三角形問題構(gòu)件中反應(yīng)三角形類型的狀態(tài)“tType”作為興趣點，對其構(gòu)件系統(tǒng)的功能依賴圖進(jìn)行切片試驗。圖4所得到的即為切片后的三角形問題構(gòu)件系統(tǒng)的功能依賴圖。

在利用基于模型檢驗的接口變異測試方法對構(gòu)件系統(tǒng)進(jìn)行驗證并生成測試用例時，為了能夠體現(xiàn)出構(gòu)件系統(tǒng)模型中存在的“狀態(tài)空間爆炸”問題以及通過切片技術(shù)對系統(tǒng)的狀態(tài)空間進(jìn)行壓縮后的效果，首先選擇三角形問題構(gòu)件的接口函數(shù)TriType（int a， int b， int c）的等價變異體TriType（int c， int b， int a）作為研究對象，并將三邊的輸入域劃分為5組進(jìn)行對比分析。

表2給出了在上述實驗條件下，JPF對切片前后的構(gòu)件系統(tǒng)在模型驗證后所得到的狀態(tài)數(shù)，它是由JPF統(tǒng)計信息中“state”里面的“new”與“visited”相加所得到的。

對表2進(jìn)行分析可知：

首先，除去最后一行對壓縮率的分析外，表格中的每一行都反應(yīng)出隨著三角形三邊輸入域的增加，整個模型檢驗過程所耗費的時間以及在驗證過程中所產(chǎn)生的狀態(tài)數(shù)都在以指數(shù)形式增加，這就體現(xiàn)了在本章最開始所提到的“狀態(tài)空間爆炸”問題。

其次，表格中的每一列說明了在對構(gòu)件接口調(diào)用關(guān)系模型運用切片技術(shù)后，模型檢驗工具在驗證過程中所耗費的時間有了一定的減少，而且在整個驗證過程中系統(tǒng)模型所產(chǎn)生的狀態(tài)空間的數(shù)量也得到了壓縮，模型檢驗的驗證效率得到了提高。

再次，由于上述五組實驗只改變了三角形問題構(gòu)件的輸入域，對于構(gòu)件系統(tǒng)模型本身并沒有進(jìn)行改變，因此，在使用相同的切片準(zhǔn)則并運用切片技術(shù)對構(gòu)件系統(tǒng)的功能依賴圖進(jìn)行切片后，所得到的系統(tǒng)模型的狀態(tài)空間壓縮率在效果上基本是相同的。

最后。上述五組實驗的驗證結(jié)果都沒有檢驗出任何反例路徑，因此，切片技術(shù)的運用并不會影響“基于模型檢驗技術(shù)的接口變異測試方法”對等價變異體的正確判定。

2.2 統(tǒng)計分析

在上一小節(jié)中，通過利用JPF對同一個等價變異體TriType（int c， int b， int a）的五組不同輸入域的檢驗，說明了運用切片技術(shù)對構(gòu)件系統(tǒng)中單個接口函數(shù)的等價變異體進(jìn)行壓縮后，依然能夠通過“基于模型檢驗技術(shù)的接口變異測試方法”對等價變異體進(jìn)行有效地判定。但是，當(dāng)同一個構(gòu)件中所有不同的接口函數(shù)在分別運用切片技術(shù)對構(gòu)件系統(tǒng)模型進(jìn)行壓縮后，上述實驗結(jié)果并不能夠說明切片技術(shù)對整個構(gòu)件系統(tǒng)的驗證以及對接口測試用例生成所產(chǎn)生的影響。因此，本小節(jié)將就這一問題作進(jìn)一步的討論。

這里，分別以三角形問題構(gòu)件中的三個狀態(tài)屬性作為興趣點對構(gòu)件系統(tǒng)進(jìn)行切片，然后三個接口函數(shù)的非等價變異體對切片后的構(gòu)件系統(tǒng)模型進(jìn)行變異并驗證。表4給出了三個接口函數(shù)在切片前后進(jìn)行變異并生成測試用例的相關(guān)驗證信息，為了能夠達(dá)到對系統(tǒng)模型狀態(tài)空間進(jìn)行窮盡搜索以及對非等價變異體生成所有測試用例的目的，這里將JPF中的搜索配置策略設(shè)置為“搜索顯示多條反例路徑”。同樣地，表3所產(chǎn)生的狀態(tài)數(shù)也是由統(tǒng)計信息“states”中“new”與“visited”相加得到的。

通過對表3可以發(fā)現(xiàn)：

首先，對于每一個需要驗證的系統(tǒng)模型來說，在運用切片技術(shù)對系統(tǒng)模型進(jìn)行切片之后，都能夠達(dá)到壓縮系統(tǒng)模型狀態(tài)空間數(shù)量，并提高驗證效率的目的。

其次，表中的數(shù)據(jù)以及實際的實驗結(jié)果說明，切片后的系統(tǒng)模型在驗證后所產(chǎn)生的反例路徑與切片之前所產(chǎn)生的反例路徑是相同的，因此，切片前后所產(chǎn)生的測試用例也是一樣的。

最后，盡管切片技術(shù)是對構(gòu)件系統(tǒng)的功能依賴圖進(jìn)行切片，但其實質(zhì)上是對構(gòu)件系統(tǒng)的狀態(tài)空間進(jìn)行縮減。由于三角形構(gòu)件系統(tǒng)中僅由一個三角形構(gòu)件組成，因此其狀態(tài)空間是由三邊的輸入域所確定，這樣，表中三組實驗所對應(yīng)的切片前的構(gòu)件系統(tǒng)模型在驗證后所產(chǎn)生的狀態(tài)空間總數(shù)是一樣的；同時，對于每一個切片后的構(gòu)件系統(tǒng)模型來說，其狀態(tài)空間是由三角形構(gòu)件中的一個狀態(tài)所決定的，而該狀態(tài)又是由相同的輸入域確定，因此在切片后，構(gòu)件系統(tǒng)模型的狀態(tài)空間總數(shù)也是一樣的。綜上所述，三組實驗的狀態(tài)空間壓縮率也是相同的。

3 結(jié)束語

目前，基于模型檢驗的測試用例生成技術(shù)作為一種新興的軟件測試方法已經(jīng)得到了測試人員的廣泛關(guān)注，但是由于模型檢驗技術(shù)中所存在的“狀態(tài)空間爆炸”問題會使得驗證的效率較為低下，因此，本文主要講解了運用切片技術(shù)對系統(tǒng)模型進(jìn)行切片從而達(dá)到壓縮系統(tǒng)模型狀態(tài)空間，并提高驗證效率的目的。

本文以構(gòu)件之間接口的交互關(guān)系為基礎(chǔ)，通過擴(kuò)展構(gòu)件之間接口交互圖后，提出了一種建立構(gòu)件系統(tǒng)的功能依賴圖的具體方法，然后運用切片算法實現(xiàn)了對其進(jìn)行切片的目標(biāo)。最后，本文通過基于模型檢驗的接口變異測試方法對三角形問題的JavaBean構(gòu)件的實驗說明：在運用切片技術(shù)對系統(tǒng)模型進(jìn)行切片以后，達(dá)到了有效壓縮系統(tǒng)狀態(tài)空間數(shù)量并提高驗證效率的目的，同時，不但可以對等價變異體模型進(jìn)行正確地判定，而且對于非等價變異體模型來說還可以正確地生成測試用例。

參考文獻(xiàn)：

[1] 林惠民， 張文輝. 模型檢測：理論，言方法與應(yīng)用[J]. 電子學(xué)報， 2002， 30（12A）： 1907-1912.

[2] 梁陳良， 聶長海， 徐寶文， 陳振宇. 一種基于模型檢驗的類測試用例生成方法[J]. 東南大學(xué)學(xué)報（自然科學(xué)版）， 2007， 37（5）： 776-781.

[3] W. Visser， C. Pasareanu， S. Khurshid. Test Input Generation with Java PathFinder[C]. Proceedings of ISSTA 2004， New York： ACM Press， July 2004， 97-107.

[4] 李必信. 程序切片技術(shù)及其應(yīng)用[M]. 北京： 科學(xué)出版社， 2006： 3.

[5] 張侹， 王璠， 韓柯， 歐陽志強. 面向構(gòu)件接口變異的模型檢驗技術(shù)研究[J]. 電腦知識與技術(shù)， 2010（6）： 1954-1956.

[6] Horwitz S B， et al. Interprocedural slicing using dependence graphs[J]. ACM Transactions on Programming Languages and Systems， 1990， 12（1）：26-60.

[7] 李賦欣. 規(guī)約和切片技術(shù)在組件測試用例生成中的研究[D]. 重慶： 重慶大學(xué)， 2007.

[8] 曹嚴(yán)元， 張為群. 一種基于CBD的軟件測試方法[J]. 計算機(jī)科學(xué)， 2005， 32（2）： 156-158.