周海將　吳軍華

(南京工業(yè)大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)系　江蘇 南京 210009)

?

基于符號執(zhí)行與混合約束求解的測試用例生成研究

周海將吳軍華

(南京工業(yè)大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)系江蘇 南京 210009)

摘要由于現(xiàn)有基于符號執(zhí)行的測試用例生成方法無法對關(guān)于字符串的測試用例生成提供有效支持，因此提出并實(shí)現(xiàn)了基于符號執(zhí)行與混合約束求解測試用例自動化生成方法。該方法利用模型檢測軟件對被測軟件源代碼進(jìn)行符號執(zhí)行，生成關(guān)于字符串與數(shù)值的混合約束集,利用字符串-數(shù)值約束求解器對約束集進(jìn)行求解，最終根據(jù)求解結(jié)果生成軟件測試用例與不可達(dá)路徑。實(shí)驗(yàn)結(jié)果表明，該方法較好地支持了關(guān)于字符串測試用例生成，且具有良好的效率與準(zhǔn)確性。

關(guān)鍵詞測試用例生成符號執(zhí)行技術(shù)混合約束求解字符串

0引言

隨著軟件業(yè)的不斷發(fā)展，主流軟件中字符串操作的占比越來越大[1]。例如Web軟件中后臺邏輯處理部分通常需要與數(shù)據(jù)庫進(jìn)行交互，其中SQL語句的動態(tài)生成主要通過字符串操作完成。此外，前端界面用于顯示的字符串變量與常量基本通過字符串操作動態(tài)地生成。而軟件測試是保證軟件質(zhì)量的重要手段，由于早期的傳統(tǒng)軟件測試方法主要針對數(shù)值與邏輯計(jì)算，對于字符串變量和字符串操作不能有效的支持，因此關(guān)于字符串的測試用例生成技術(shù)逐漸成為國內(nèi)外的研究熱點(diǎn)之一[2]。

1研究現(xiàn)狀

近年來軟件測試領(lǐng)域基于符號執(zhí)行的測試研究成為熱點(diǎn)。它是一種靜態(tài)程序分析技術(shù)[3]，主要原理是使用符號變量代替實(shí)際值模擬程序的執(zhí)行，獲取相應(yīng)路徑的約束，最終通過約束求解獲得測試數(shù)據(jù)。如今該技術(shù)的瓶頸在于約束求解器的效率，尤其缺乏優(yōu)秀的字符串求解器。關(guān)于約束求解技術(shù)，根據(jù)表示字符串的形式，字符串約束求解器主要分為基于位向量與基于有限狀態(tài)自動機(jī)兩種類型。

HAMPI[4]是基于位向量的字符串約束求解器，主要原理是將輸入的字符串約束轉(zhuǎn)換為是否為正則語言接受的形式，利用位向量表示，最后利用STP位向量求解器求解約束條件。但僅支持固定長度的字符串約束且不支持?jǐn)?shù)值約束。Kudzu[5]基于位向量，改進(jìn)了HAMPI，提供了較多字符串操作的支持，并且有限支持?jǐn)?shù)值約束。

文獻(xiàn)[2]詳細(xì)論述了基于有限狀態(tài)自動機(jī)的字符串約束求解器技術(shù)。其中Rex[7]基于有限狀態(tài)機(jī)與SMT約束求解器，使用邏輯謂語表示自動機(jī)的轉(zhuǎn)換。Rex支持字符串約束與數(shù)值約束，但效率很低，遠(yuǎn)遠(yuǎn)慢于HAMPI。文獻(xiàn)[8]提出一種基于怠惰算法的約束求解技術(shù)，利用圖表示字符串之間的約束，通過回溯搜索圖尋求結(jié)果。該技術(shù)若有解時(shí)，效率很高；若無解則求解時(shí)間往往超出可接受范圍。此外，該技術(shù)只能對字符串操作與正則語言提供有限的支持。

綜上所述，要實(shí)現(xiàn)基于符號執(zhí)行軟件測試自動化，就應(yīng)改進(jìn)約束求解技術(shù)的效率與增強(qiáng)適用性。

2符號執(zhí)行與約束求解

符號執(zhí)行[3]是一種可靠的程序分析技術(shù)，基本原理是：在源代碼中，將程序中變量值替換為表示為未知但固定的符號標(biāo)記，模擬程序執(zhí)行的過程。符號標(biāo)記在靜態(tài)數(shù)學(xué)意義上用來表示一些未知的但固定的值，一個(gè)程序在特定的執(zhí)行過程中會有與其相關(guān)的多個(gè)不同的符號標(biāo)記。主要思想是從控制流圖的入口處用符號標(biāo)記代替具體的輸入值來模擬程序符號化的執(zhí)行過程。一般的軟件測試用具體值作為測試用例輸入來執(zhí)行程序，所進(jìn)行的計(jì)算是具體邏輯運(yùn)算，符號執(zhí)行使用符號標(biāo)記來執(zhí)行程序，所進(jìn)行的是代數(shù)運(yùn)算，符號執(zhí)行即一般測試的擴(kuò)充。符號執(zhí)行是程序驗(yàn)證和程序測試的折中，一方面它具有普通測試所具有的測試方法，通過運(yùn)行被測程序驗(yàn)證程序的可靠性；另一方面，符號執(zhí)行沿著一條路徑的一次執(zhí)行積累的約束條件代表了一大類普通測試的集合，驗(yàn)證程序接受此類輸入后是否正確，同時(shí)可以發(fā)現(xiàn)程序中不可行的路徑。

約束問題由三個(gè)基本元素組成：變量、變量域與約束。約束求解即在變量域中找到特定變量值使之與各變量之間均滿足約束?；旌霞s束問題是傳統(tǒng)約束問題的擴(kuò)展，即變量域?yàn)槎鄠€(gè)，本文分為數(shù)值變量域與字符串變量域。約束求解技術(shù)主要包括數(shù)值法、符號計(jì)算法、區(qū)間分析法、啟發(fā)式算法等。

3基于符號執(zhí)行與混合約束求解的測試用例生成技術(shù)

3.1符號執(zhí)行框架

本文提出了一個(gè)基于符號執(zhí)行技術(shù)與混合約束求解的測試用例自動化生成方法框架，總體來說包括兩個(gè)部分：符號執(zhí)行生成約束部分；對約束集求解得到測試輸入與不可達(dá)路徑部分。主要步驟為：

(1) 將源程序進(jìn)行擴(kuò)展，利用符號執(zhí)行工具對已擴(kuò)展的源代碼進(jìn)行符號執(zhí)行，遍歷源程序的每個(gè)路徑，生成每個(gè)與程序終點(diǎn)相對應(yīng)的路徑條件。路徑條件定義為與該程序終點(diǎn)對應(yīng)的約束。這樣的過程最后得到的就是路徑條件集合，即約束條件集合。

(2) 利用約束求解方法對約束條件集合進(jìn)行約束求解，得到關(guān)于每個(gè)程序終點(diǎn)的約束的具體值，即程序測試輸入。若約束求解無解，即程序終點(diǎn)不可達(dá)，說明該路徑是錯(cuò)誤的，返回該錯(cuò)誤路徑。符號執(zhí)行框架的結(jié)構(gòu)如圖1所示。

圖1　基于符號執(zhí)行與混合約束求解測試用例生成框架

本文對基于符號執(zhí)行與混合約束求解測試用例生成框架給出以下定義:

定義 1定義執(zhí)行該路徑得到的路徑條件為PC(Path Condition)，PC積累了該路徑每一條語句執(zhí)行必須滿足的約束。不可達(dá)路徑的執(zhí)行路徑定義為PU。

定義2約束集C：定義由對源程序進(jìn)行符號執(zhí)行得到的路徑集合為C{c1,….,ci,….,cn},稱C為約束條件集合，其中ci表示某個(gè)具體的路徑條件表達(dá)式，n為約束條件的總數(shù)。

定義3若是關(guān)于數(shù)值的路徑條件，定義為數(shù)值約束PCN；若是關(guān)于字符串的約束，定義為字符串約束PCS；若PC中既包含數(shù)值約束又包含字符串約束，稱該P(yáng)C為混合約束條件PCH，對于混合約束條件集合為CH。

定義4由PCN求解得到的值為關(guān)于數(shù)值約束條件的測試輸入，定義為TN;由PCS求解得到的值為關(guān)于字符串約束條件的測試輸入，定義為TS;相應(yīng)的TN與TS的集合即關(guān)于該執(zhí)行路徑的測試輸入T。

定義5由對約束條件集合進(jìn)行求解的過程定義為S，其中S的輸入是約束條件集合，輸出為測試輸入集合與不可達(dá)路徑條件。表達(dá)式為：

S(C)=TANDPU

其中C={c1,…,ci,…,cN};T={T1,…，Ti,…，TN}，Ti=TNiANDTSi。

3.2路徑條件生成

本文將通過圖2的例子詳細(xì)論述符號執(zhí)行的過程。圖2表示的是根據(jù)字符串取值的不同采取不同處理，目的是對字符串進(jìn)行辨識以確定S的含義，并決定采取哪些方法處理S。

圖2　路徑條件的分支樹

如圖2所示，PC0表示的是符號執(zhí)行的起點(diǎn)，Path1-Path6表示的是符號路徑的終點(diǎn)。符號L(q)代表字符串q的長度。符號執(zhí)行過程中，首先檢測輸入字符串是否以負(fù)號為開頭，即檢測字符串s代表的是否為負(fù)數(shù)；接著檢測字符串是否符合正則表示式的格式；然后檢測字符串s中是否含有逗號，若無逗號，字符串s將被轉(zhuǎn)換為長精度類型，否則將s中逗號后面的數(shù)字賦值整型變量x;最后檢測x是否小于100。這個(gè)代碼在一般的Web程序中比較常見，首先對輸入字符串進(jìn)行格式檢測，接著將字符串轉(zhuǎn)換為數(shù)字，最終在分支中對字符串進(jìn)行處理。在每個(gè)路徑終點(diǎn)都生成了約束條件的交集，即通過符號執(zhí)行得到的約束條件集合C，其中C中元素為：

c1={s.charAt(0)==’-’}

c2={ s.charAt(0)==’-’,s.matches(“-d+,d{3}”)}

c3={s.charAt(0)==’-’,s.notmatches(“-d+,d{3}”,s.notCtains(“,”),i==-1,f==VOF(s),f1==(f/102),round(f1/3)=dl}

c4={s.charAt(0)==’-’,s.notmatches(“-d+,d{3}”,s.notCtains(“,”),i==-1,f==VOF(s),f1==(f/102),round(f1/3)≠dl}

c5={s.charAt(0)==’-’,s.notmatches(“-d+,d{3}”,s.subString(i,i+1)==”,”sl=s.substring(i+1),VOF(sl)>=100 }

c6={s.charAt(0)==’-’,s.notmatches(“-d+,d{3}”,s.subString(i,i+1)==”,”sl=s.substring(i+1),VOF(sl)<100 }

在下一步中通過對C進(jìn)行約束求解，則可以生成測試數(shù)據(jù)與不可達(dá)路徑。由于C中的元素ci既包含PCN又包含PCS，因此，約束求解器就需要具有對PCN和PCS兩種約束條件的求解能力。當(dāng)前的約束求解算法對字符串約束不能提供有效支持，對此本文提出并實(shí)現(xiàn)了數(shù)值—字符串混合約束求解器[9]。

3.3混合約束求解算法

混合約束集合包含數(shù)值約束與字符串約束。本文對此的解決方法為：通過將兩種約束集進(jìn)行分離，運(yùn)用不同的約束求解器進(jìn)行處理。數(shù)值約束條件選用已有的Coral[10]方法和Yices[11]方法處理，其中線性數(shù)值約束使用Yices方法處理，簡單非線性數(shù)值約束使用Coral方法處理。對于字符串約束條件使用本文設(shè)計(jì)的基于有限狀態(tài)機(jī)(FSM)約束求解器。具體算法為：

步驟1初始化約束求解器。加載由符號執(zhí)行步驟得到的約束條件集合CH。對CH中的所有元素ci遍歷執(zhí)行以下步驟。

步驟2利用Coral與Yices數(shù)值約束求解器對ci中的PN部分進(jìn)行求解，若無解則輸出該執(zhí)行路徑，并退出；若有解，保存Ts并執(zhí)行下一步。

步驟3將CH中的Cs部分加載到求解器中，并對其進(jìn)行字符串求解。若有解則輸出Ts與Tn。即該執(zhí)行路徑的測試輸入；若無解，執(zhí)行以下步驟。

步驟4首先判斷求解時(shí)間是否超出限制，若超出則放棄，返回求解時(shí)間并退出；反之，根據(jù)RULE庫替換可以替換的字符串約束條件為相應(yīng)的數(shù)值約束條件，轉(zhuǎn)到步驟1循環(huán)。

在算法中提到的RULE庫是為了提高混合約束條件求解效率而增加的。主要實(shí)現(xiàn)的原理:字符串約束部分可以轉(zhuǎn)換為數(shù)值約束，數(shù)值約束求解效率一般優(yōu)于字符串約束期間效率，實(shí)現(xiàn)部分?jǐn)?shù)值約束與字符串約束互相的轉(zhuǎn)換將提高求解效率。

3.4字符串約束求解改進(jìn)

本文使用有限狀態(tài)機(jī)(FSM)表示一個(gè)符號字符串變量，即所有變量可能的取值組成了可以被這個(gè)FSM識別的語言。實(shí)現(xiàn)是基于文獻(xiàn)[12]提出的自動機(jī)。FSM的轉(zhuǎn)換(邊)擁有一個(gè)范圍取值。當(dāng)一個(gè)自動機(jī)求精時(shí)，不僅需要改變結(jié)點(diǎn)和邊，邊上的額外取值范圍也會變化。例如圖3表示的是接受正則表達(dá)式“-d+,d{3}”的自動機(jī)。

圖3　接受-d+,d{3}的自動機(jī)

本文通過使用有限狀態(tài)自動機(jī)來實(shí)現(xiàn)字符串的操作。例如，字符串s1和字符串s2的連接操作轉(zhuǎn)換為s2的自動機(jī)附加到s1自動機(jī)的操作。該自動機(jī)支持了很多的字符串操作，但是因?yàn)槠湓O(shè)計(jì)是用于靜態(tài)分析，本文擴(kuò)展該自動機(jī)不支持的字符串操作。例如，substring(2,4)方法的操作返回的是從索引位置2到索引位置4的子字符串，如圖4所示?；痉椒ㄊ牵菏紫葟拈_始狀態(tài)轉(zhuǎn)移兩個(gè)步驟；然后將訪問到的節(jié)點(diǎn)作為開始節(jié)點(diǎn)；接著將從開始節(jié)點(diǎn)兩步轉(zhuǎn)換中所有的狀態(tài)作為接受狀態(tài)；最后，我們交互該自動機(jī)并接受所有長度為2的自動機(jī)用來得到最終的自動機(jī)版本。除此之外還有其他需要擴(kuò)展，比如替換字符與替換子字符串等。

圖4　在自動機(jī)上操作substring(2,4)操作

字符串約束描述的是字符串之間的關(guān)系。FSM并不直接對字符串約束求解，因此需要根據(jù)字符串約束加強(qiáng)對字符串的求精。這個(gè)過程包括：(1)自動機(jī)求精；(2)不動點(diǎn)計(jì)算；(3)優(yōu)化收斂速度。例如，對于s.charAt(0)=’-’約束，將字符串s與接收首字符為負(fù)號的自動機(jī)交互。后來，因?yàn)樽址畇的部分通過parseInt方法轉(zhuǎn)換為整型變量，將字符串s的該部分與建模所有有效整數(shù)交互；同樣需要對字符串s的根據(jù)更新部分對字符串s進(jìn)行求精。例如，將字符串s的自動機(jī)與以某種形式結(jié)尾部分的自動機(jī)交互。這部分工作將一直進(jìn)行，直到?jīng)]有什么求精是可能的，并且得到不動點(diǎn)，即得到一個(gè)可能的字符串值。

本文通過RULE庫來實(shí)現(xiàn)字符串約束與數(shù)值約束之間的互相轉(zhuǎn)換，因此字符串約束和數(shù)值約束對于共享的符號變量取值必須一致，即共享的符號變量在數(shù)值約束與字符串約束中的值相同。在符號變量同步的過程中，數(shù)值約束求解器N會給出一些候選值，提交給字符約束求解器S判斷該符號變量值是否沖突。若無沖突，則符號變量取值被S和N都接受；否則S會返回N引起沖突的約束變量值，請求N提交其他候選符號變量取值。接著N取消沖突的符號變量值，使用啟發(fā)式算法重新搜索另一個(gè)有效賦值，繼續(xù)以上步驟。在交互的過程中只有共享變量的具體值可以從N提交到S，N也可以理解一些字符串沖突，并傳遞給S。例如，數(shù)值約束s.length()>5使相應(yīng)的自動機(jī)應(yīng)該與接受長度大于5的自動機(jī)交互。

在迭代過程中，我們將字符串約束求解器[14，15]和數(shù)值約束求解器得到的約束交換，這樣就可以提高收斂速度。例如，對于字符串約束s1=s2.trim()，數(shù)值約束求解器會給出一個(gè)數(shù)值約束給出L(s1)<=L(s2)，其中L()方法返回的是字符串對象的長度。

在方法中，類似上例的交互約束由RULE庫建模，RULE庫包含一般Java程序常見的交互規(guī)則，表1展示了該庫的部分規(guī)則。

表1　RULE庫中部分RULE規(guī)則

續(xù)表1

為了解釋數(shù)值與字符串約束迭代求解的過程，對于圖2中的path 4,下面給出了path 4的路徑條件，包含了已經(jīng)增加的額外的約束。為了對該約束求解，數(shù)值約束求解器將得到一組有效的數(shù)值變量賦值，L(s)=2,L(s1)=1,i=0,x=100。然后將這組賦值提交給字符串約束求解器。但是因?yàn)閤=parseInt(s1)條件不滿足，所以字符串求解器沒有找到有效賦值。這就要求N進(jìn)行重新計(jì)算直到s1的長度大于等于3，或者求解器利用RULE庫從“x=parseInt(s1) ^ 》100”得到一個(gè)額外的L(s1)>=3約束。此外從“s1 = s.substring(i+1)”得到L(s)>=L(s1)。有了額外的約束，求解器可以很快得到新的一組有效變量賦值，例如s=“-,100”, s1=“100”, i=1,x=100。

NumericString

(1 : L(s) > 0)s:charAt[0] = `-’

(3 : i + 1 + L(s1) = L(s))s1 = s.substring(i + 1)

(4 : L(s1) > 0)x = parseInt(s1)

i=≠-1 ^ x》 100┐(s.matches(- d+,d{3}))

當(dāng)字符串約束求解器S不能得到一個(gè)有效賦值時(shí)，額外的約束被傳遞給數(shù)值約束求解器并始新的迭代計(jì)算。最終，混合約束迭代求解器可以得到一個(gè)有效的解決。

在符號執(zhí)行得到的混合約束可能包含非線性數(shù)值約束條件，對非線性約束求解，正常的處理不僅效率不高，而且容易導(dǎo)致約束求解失敗。對此本文通過將非線性約束條件轉(zhuǎn)換為多個(gè)線性約束組合來避免直接求解效果不佳。例如round()方法，該方法的作用是對于給定的浮點(diǎn)數(shù)變量返回最接近的整型值。對于round()方法，本文將其轉(zhuǎn)換為“((e-0.5 =x1))^((e-0.5<=x2)^(e+ 0.5 >x2))^(result= (if(e> 0)x1x2 ))”。其中e為實(shí)數(shù)，x1、x2和result是引進(jìn)的整型變量，result代表的round(e)的返回值。同樣地，將其他的一些約束進(jìn)行類似的轉(zhuǎn)換，用以處理非線性數(shù)值約束。

4實(shí)驗(yàn)部分

本文使用的是兩個(gè)富含字符串操作的Java源程序進(jìn)行對比試驗(yàn)，使用JPF的符號執(zhí)行版本[13]對實(shí)驗(yàn)樣本進(jìn)行符號執(zhí)行兩個(gè)程序的詳細(xì)情況見表2。由于程序代碼量過大，因此僅關(guān)注邏輯處理部分，因?yàn)檫@部分代表了程序中最復(fù)雜的字符串與數(shù)值計(jì)算與處理。測試環(huán)境為HPPC機(jī)-IntelCore2DuoCPUE7500,2.93GHz,2GB;WindowsXPsp3。

表2　實(shí)驗(yàn)程序數(shù)據(jù)

測試中記錄生成的是輸入符號變量的個(gè)數(shù)，在程序有效結(jié)束狀態(tài)下生成的測試用例個(gè)數(shù)，在符號執(zhí)行中因異常拋出而未執(zhí)行的路徑個(gè)數(shù)。完成實(shí)驗(yàn)的時(shí)間、完成實(shí)驗(yàn)中迭代的次數(shù)見表3所示。最后在符號輸入個(gè)數(shù)為四個(gè)時(shí)，得到了的測試用例覆蓋率達(dá)到80%。

表3　程序A的實(shí)驗(yàn)結(jié)果

由表3可以看出在符號輸入個(gè)數(shù)為4時(shí)，得到了的測試用例覆蓋率達(dá)到80%。綜上所述，該技術(shù)在合理的時(shí)間內(nèi)能有效自動化地生成測試用例與不可達(dá)路徑。

為了說明非線性約束求解的有效性，本文使用金融應(yīng)用程序B進(jìn)行單元測試。程序B包含很多對Java語言長精度類型的舍入操作。實(shí)驗(yàn)對非線性模式開啟與否做了多次實(shí)驗(yàn)(如表4所示)。當(dāng)開啟非線性模式時(shí)，所有生成的路徑條件由Yices求解，反之則由Coral求解。可以從表中明顯看到，非線性模式下的具有明顯優(yōu)勢。

表4　程序B的實(shí)驗(yàn)結(jié)果

從表3、表4可以看出，本文提出的基于符號執(zhí)行與混合約束求解技術(shù)的測試自動化技術(shù)明顯優(yōu)于傳統(tǒng)基于符號執(zhí)行的測試自動化技術(shù)。不僅對字符串約束與數(shù)值約束提供支持，求解效率也有明顯提升。

5結(jié)語

本文對符號執(zhí)行技術(shù)、數(shù)值—字符串混合約束求解進(jìn)行了研究，設(shè)計(jì)并實(shí)現(xiàn)了基于符號執(zhí)行和混合約束求解的自動化測試技術(shù)。它能有效提高約束求解效率，并支持字符串約束與數(shù)值約束。實(shí)驗(yàn)表明，該方法能在可接受的時(shí)間范圍內(nèi)生成測試

用例與錯(cuò)誤路徑。文中的混合約束求解框架還有一些不足與需要改進(jìn)的算法?；旌霞s束求解算法的效率還存在提高的可能，優(yōu)化可以采用各個(gè)擊破的“on-the-fly”技術(shù)。此外該方法只能對Java源程序提供支持，以后可以擴(kuò)展到其他主流編程語言例如C++、C等。

參考文獻(xiàn)

[1] 梅宏,王嘯吟,張路.字符串分析研究進(jìn)展[J].軟件學(xué)報(bào),2012,24(13):37-49.

[2]HooimeijerP,VeanesM.Anevaluationofautomataalgorithmsforstringanalysis[C]//Verification,ModelChecking,andAbstractInterpretation.SpringerBerlinHeidelberg, 2011: 248-262.

[3]KingJC.Symbolicexecutionandprogramtesting[J].CommunicationsoftheACM, 1976, 19(7): 385-394.

[5]SaxenaP,AkhaweD,HannaS,etal.Asymbolicexecutionframeworkforjavascript[C]//SecurityandPrivacy(SP), 2010IEEESymposiumon.IEEE, 2010: 513-528.

[6]VeanesM,DeHalleuxP,TillmannN.Rex:Symbolicregularexpressionexplorer[C]//SoftwareTesting,VerificationandValidation(ICST), 2010ThirdInternationalConferenceon.IEEE, 2010: 498-507.

[7]HooimeijerP,WeimerW.Solvingstringconstraintslazily[C]//ProceedingsoftheIEEE/ACMinternationalconferenceonAutomatedsoftwareengineering.ACM, 2010: 377-386.

[8]ShannonD,GhoshI,RajanS,etal.Efficientsymbolicexecutionofstringsforvalidatingwebapplications[C]//Proceedingsofthe2ndInternationalWorkshoponDefectsinLargeSoftwareSystems:HeldinconjunctionwiththeACMSIGSOFTInternationalSymposiumonSoftwareTestingandAnalysis(ISSTA2009).ACM, 2009: 22-26.

[9]SouzaM,BorgesM,d’AmorimM,etal.CORAL:solvingcomplexconstraintsforsymbolicpathfinder[M]//NASAFormalMethods.SpringerBerlinHeidelberg, 2011: 359-374.

[10]DutertreB,DeMouraL.Theyicessmtsolver[OL]. 2006.Toolpaperathttp://yices.csl.sri.com/tool-paper.pdf.

[11]ChristensenAS,M?llerA,SchwartzbachMI.Preciseanalysisofstringexpressions[M].SpringerBerlinHeidelberg, 2003.

[12]P?s?reanuCS,RungtaN.SymbolicPathFinder:symbolicexecutionofJavabytecode[C]//ProceedingsoftheIEEE/ACMinternationalconferenceonAutomatedsoftwareengineering.ACM, 2010: 179-180.

ON TEST CASE GENERATION BASED ON SYMBOLIC EXECUTION AND HYBRID CONSTRAINT SOLVING

Zhou HaijiangWu Junhua

(Department of Computer Science and Technology, Nanjing Tech University, Nanjing 210009, Jiangsu, China)

AbstractSince current test case generation method based on symbolic execution is unable to provide effective support to the test case generation with regard to character string, therefore we present an automatic test case generation method, which is based on symbolic execution and hybrid constraint solving, and implement it as well. The method uses the model checking software to make symbolic execution on the source code of the software to be tested and generates a mixed constraint set correlated to string and numeral. Then it uses the string-numerical constraints solver to calculate the constraint set. Finally, according to the calculation result it generates the software test case and the infeasible path. Experimental result shows that this method well support the generation of test case in regard to string and has good efficiency and accuracy.

KeywordsTest cases generationSymbolic execution technologyHybrid constraint solvingString

收稿日期：2015-01-30。周海將，碩士，主研領(lǐng)域：軟件測試。吳軍華，副教授。

中圖分類號TP301

文獻(xiàn)標(biāo)識碼A

DOI:10.3969/j.issn.1000-386x.2016.06.006