龍慶　王璠

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

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

中圖分類號(hào)：TP311 文獻(xiàn)標(biāo)識(shí)碼：A 文章編號(hào)：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

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

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

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

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

S.Horwitz等人通過(guò)引入系統(tǒng)依賴圖（System Dependence Graph，SDG）的概念表示了具有多個(gè)過(guò)程的程序依賴圖[6]，但是使用該方法就必須知道每一個(gè)過(guò)程內(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)件之間的接口交互圖后，使其能夠在清晰描述源碼未知情況下被測(cè)試構(gòu)件的狀態(tài)和接口函數(shù)之間的關(guān)系的同時(shí)，也能夠使切片技術(shù)適用于對(duì)被測(cè)試構(gòu)件系統(tǒng)的接口調(diào)用關(guān)系模型的狀態(tài)空間的壓縮。

1.1 功能依賴圖的組成

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1） 測(cè)試驅(qū)動(dòng)程序?qū)?gòu)件的實(shí)例化

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

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

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

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

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

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

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

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

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

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

2 實(shí)驗(yàn)結(jié)果和分析

2.1 實(shí)驗(yàn)對(duì)象說(shuō)明及實(shí)驗(yàn)結(jié)果

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

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

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

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

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

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

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

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

2.2 統(tǒng)計(jì)分析

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

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

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

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

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

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

3 結(jié)束語(yǔ)

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

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

參考文獻(xiàn)：

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

[2] 梁陳良， 聶長(zhǎng)海， 徐寶文， 陳振宇. 一種基于模型檢驗(yàn)的類測(cè)試用例生成方法[J]. 東南大學(xué)學(xué)報(bào)（自然科學(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] 張侹， 王璠， 韓柯， 歐陽(yáng)志強(qiáng). 面向構(gòu)件接口變異的模型檢驗(yàn)技術(shù)研究[J]. 電腦知識(shí)與技術(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ù)在組件測(cè)試用例生成中的研究[D]. 重慶： 重慶大學(xué)， 2007.

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