一種基于Actor模型的并行動態(tài)符號執(zhí)行方法

張曉文,賈向陽,常 亮,劉錢超,胡小輝

1(桂林電子科技大學 廣西可信軟件重點實驗室,廣西 桂林 541004) 2(武漢大學 軟件工程國家重點實驗室,武漢 430000)

1 引 言

符號執(zhí)行技術(shù)是一種經(jīng)典的程序分析技術(shù).它使用符號值來代替具體的值來模擬執(zhí)行程序,系統(tǒng)化地探索程序的可行的路徑,從而來發(fā)現(xiàn)難以發(fā)現(xiàn)的缺陷,以及為各個路徑生成測試用例[1-3].動態(tài)符號執(zhí)行技術(shù)(如Concolic Testing[9-13]和Dart[5,8])在符號執(zhí)行中引入了具體值,利用具體值執(zhí)行程序,記錄程序中的符號值和各個分支的路徑條件(Path Condition).在一條路徑執(zhí)行完成后,通過對其它分支的路徑條件進行約束求解,來生成針對新路徑的程序輸入,引導下一次執(zhí)行.

動態(tài)符號執(zhí)行相對靜態(tài)符號執(zhí)行具有更高的效率,因此在目前得到了更廣泛的應(yīng)用.然而,由于動態(tài)符號執(zhí)行同樣需要探索大量的路徑,并進行耗時的約束求解,因此對于稍大規(guī)模的程序,效率往往難如人意[4].

將符號執(zhí)行中耗時的工作并行化是提高效率的有效手段.目前國內(nèi)外也有一些此類的探索工作[6,7].然而,符號執(zhí)行的并行優(yōu)化仍然面臨著一些挑戰(zhàn)性的問題:

1)任務(wù)的動態(tài)迭代式產(chǎn)生問題:在動態(tài)符號執(zhí)行中,路徑探索和約束求解這些耗時的工作是動態(tài)迭代式產(chǎn)生的:每求解路徑條件并探索完一條路徑后,都會產(chǎn)生一組新路徑需要進行約束求解和路徑探索.這種動態(tài)迭代式的任務(wù),很難通過靜態(tài)任務(wù)分配方式來實現(xiàn)并行化.

2)大規(guī)模任務(wù)的通信代價問題:動態(tài)符號執(zhí)行中路徑探索和約束求解的任務(wù)數(shù)據(jù)巨大,單個任務(wù)則一般執(zhí)行時間并不長.這種大規(guī)模的小任務(wù)對任務(wù)調(diào)度的通信代價具有很高的敏感性.

本文針對上述問題,提出了一種基于Actor并行模型的動態(tài)符號執(zhí)行并行優(yōu)化方法.該方法將符號執(zhí)行中的任務(wù)按照符號執(zhí)行樹的子樹方式分配到多個獨立運行的Actor工作節(jié)點中.各個Actor工作節(jié)點負責對該子樹的路徑條件進行求解,對可行路徑進行探索.每條路徑探索完然后發(fā)現(xiàn)新路徑時,將新增加的路徑數(shù)目通知調(diào)度中心.調(diào)度中心監(jiān)控各個節(jié)點的路徑數(shù)目,如果某個節(jié)點處于空閑狀態(tài)時,則從最多路徑的節(jié)點“拆借”一個子樹分配給該節(jié)點,從而實現(xiàn)了任務(wù)的動態(tài)負載均衡.工作節(jié)點向調(diào)度中心發(fā)送路徑數(shù)時采用異步方式,并且數(shù)據(jù)量很小,通信代價基本可以忽略.由于各個工作節(jié)點只探索相對獨立的路徑子樹,基本兼容了之前的符號執(zhí)行工作模式,因此已有的優(yōu)化機制仍然可以很方便地整合使用.

2 基于Actor模型的并行符號執(zhí)行方法

2.1 Actor模型

Actor模型是一種經(jīng)典的并行計算模型,在Actor模型中,Actor是一種可以響應(yīng)外部消息的計算實體[19].異步消息是Actor之間唯一的通信方式.Actor模型中各個Actor可以并行執(zhí)行計算任務(wù),但各個Actor又相互獨立運行,沒有鎖機制等依賴關(guān)系.

Actor模型等這些特點非常符合并行符號執(zhí)行的特定需求.各個并行計算節(jié)點做為Actor可以不依賴其他節(jié)點、相對獨立地執(zhí)行局部任務(wù).而異步消息保證了通信不會影響本節(jié)點的計算工作.

2.2 方法概述

總體框架設(shè)計如圖1所示,由Master和多個Worker組成.方法使用了兩種類型的Actor:MasterActor和WorkerActor.主要功能是:

1)MasterActor:負責負載均衡和任務(wù)分配.該部分維護一個負載表,記錄每個Worker發(fā)送來的負載消息.任務(wù)中心會根據(jù)負載表判斷是否需要啟動負載均衡工作(負載值超過負載表中任務(wù)的負載最大值),若需要則會給負載大的Worker節(jié)點發(fā)送任務(wù)轉(zhuǎn)移消息,收到相應(yīng)消息后會將任務(wù)發(fā)送給給空閑的工作節(jié)點,以此實現(xiàn)多個節(jié)點的任務(wù)均衡分配.

2)WorkerActor:負責對程序某個特定的路徑子樹進行符號執(zhí)行.節(jié)點維護一個維護待求解路徑棧和一個待探索路徑棧.該部分實現(xiàn)了worker內(nèi)部約束求解和路徑探索的并行工作:worker節(jié)點響應(yīng)MasterActor提供的任務(wù),放入待求解路徑棧中,約束求解器從棧中讀取任務(wù),進行求解,求解后的路徑放入待探索路徑棧中.路徑探索模塊從待探索路徑棧中讀取路徑進行探索,探索完成后,又會產(chǎn)生新的一組路徑,放入待求解路徑棧中.依次迭代直到所有的路徑都探索完成,或者找到滿足目標的路徑.

工作節(jié)點在每次路徑探索結(jié)束后,會將當前的兩個棧中的任務(wù)數(shù)作為結(jié)點的負載發(fā)給MasterActor.而MasterActor如果需要負載均衡的時候,忙節(jié)點的WorkerActor會將當前未探索的子樹轉(zhuǎn)移到空閑節(jié)點上,來實現(xiàn)負載均衡.

2.3 基于子樹轉(zhuǎn)移的動態(tài)負載均衡方法

由于在動態(tài)符號執(zhí)行中,待探索的路徑是動態(tài)迭代式產(chǎn)生的,因此很難準確評估各個節(jié)點的負載,從而實現(xiàn)精確的負載均衡.本文中采取了動態(tài)負載均衡方法,只有存在空閑節(jié)點時,才從繁忙的節(jié)點處拆借任務(wù)到空閑節(jié)點上.這樣保證各個節(jié)點都處于工作狀態(tài),達到一定程度上的負載均衡.

在本文中,節(jié)點的負載表示為待求解路徑棧和待探索路徑棧中的總路徑數(shù)目.每一條路徑探索完成后,可能會產(chǎn)生新路徑,放入待求解路徑棧中,從而使節(jié)點的負載發(fā)生變化.這時,工作節(jié)點會將新的負載發(fā)送到Master節(jié)點.當子樹的最后一條路徑探索完成,沒有新路徑產(chǎn)生時,節(jié)點的負載變?yōu)?.

當負載為0的節(jié)點出現(xiàn)后,Master節(jié)點會啟動負載均衡,查找負載最大的節(jié)點,進行路徑轉(zhuǎn)移.為了避免分析后期階段少量任務(wù)的多次轉(zhuǎn)移.我們?yōu)楣?jié)點設(shè)置了一個最少負載,只有超過這個最少負載的節(jié)點才會拆借出子樹給空閑節(jié)點.

在工作節(jié)點中,取待求解路徑棧和待探索路徑棧中的路徑實際上代表了一個未展開的子樹.在進行子樹轉(zhuǎn)移時,實際上就是取路徑棧中的某個路徑轉(zhuǎn)移給其他節(jié)點.然而,具體選擇哪個子樹進行轉(zhuǎn)移,需要根據(jù)分析的目標和算法,設(shè)定不同的策略來確定.例如,為了避免轉(zhuǎn)移了過小子樹造成過于頻繁的負載均衡,我們可以取待求解路徑棧中長度最短的路徑進行轉(zhuǎn)移.在深度優(yōu)先搜索中,長度最短路徑就是棧底的路徑.或者,為了在啟發(fā)式搜索中更快地找到目標,我們可以將接近棧頂?shù)穆窂竭M行轉(zhuǎn)移,因為這些路徑找到目標的可能性較大.

圖2 子樹轉(zhuǎn)移Fig.2 Subtree shifting

如圖2所示,當左邊節(jié)點需要轉(zhuǎn)移任務(wù)到右邊節(jié)點時.由于路徑樹中A是根節(jié)點,A的左子樹正在探索,而右子樹(節(jié)點B是根節(jié)點)是未探索的子樹.該節(jié)點代表的路徑目前存放在待求解路徑棧中.于是B開始的子樹將被轉(zhuǎn)移到右邊的空閑節(jié)點上,進行約束求解和生成待探索路徑.轉(zhuǎn)移后,左節(jié)點將不再探索B節(jié)點代表的子樹.

空閑節(jié)點會出現(xiàn)在兩個時間點:

1)并行符號執(zhí)行剛最開始啟動時,路徑樹的根節(jié)點被分配給一個工作節(jié)點進行分析,其他節(jié)點處于空閑狀態(tài).

2)某個節(jié)點分析的子樹的所有路徑都探索完成時,當前節(jié)點的負載為0,稱為空閑節(jié)點.

2.4 路徑探索與約束求解的并行

原始符號執(zhí)行是路徑探索和約束求解分別執(zhí)行,當程序執(zhí)行時將所有的待求解的路徑探索出來,然后使用約束求解器將探索路徑進行求解,但是這樣的模式對于大規(guī)模程序而言,耗時較長,嚴重浪費系統(tǒng)資源.針對上述問題,提出路徑探索和約束求解并行執(zhí)行,這樣可以節(jié)省程序執(zhí)行時間.

圖3 并行路徑探索與約束求解Fig.3 Parallel path exploration and constraint solving

如圖3所示，包含兩個棧:待求解路徑棧和待探索路徑棧;節(jié)點A為路徑的根節(jié)點;節(jié)點B為未展開節(jié)點;P1、P2等是待求解路徑棧;P7、P8等是待探索路徑棧;并行路徑探索和約束求解是通過該棧相互操作,實現(xiàn)任務(wù)的并行操作.當執(zhí)行路徑操作時,首先將待求解的路徑存入待求解路徑棧,空閑節(jié)點從該棧中取相應(yīng)任務(wù),然后通過約束求解器Z3將待求解路徑進行求解操作,同時生成待探索路徑,存入待探索路徑棧,進行路徑探索,探索完成后,產(chǎn)生的新路徑又會存放到待求解任務(wù)棧中,這樣遞歸完成對所有路徑的探索和求解.待探索任務(wù)棧中會不停的存和取任務(wù),而待探索任務(wù)棧會根據(jù)求解結(jié)果存放路徑,這樣,可以并行完成任務(wù)操作.

3 實驗與評估

我們基于動態(tài)符號執(zhí)行工具Jdart和Jdart Actor框架,實現(xiàn)了一個并行動態(tài)符號執(zhí)行原型工具Jdart-parallel.我們將Jdart-parallel較原來Jdart符號執(zhí)行效率進行對比,來評估本文方法的有效性.同時,對Jdart-parallel符號執(zhí)行工具在不同節(jié)點數(shù)下的執(zhí)行效率進行了評估,分析并行的規(guī)模對效率的作用效果.

3.1 實驗環(huán)境

本實驗主要是使用6個計算機節(jié)點操作,每一個節(jié)點的配置如下:Dell臺式電腦、Intel Core i7-4790、CPU:3.6GHz、8GB RAM 、Windows 操作系統(tǒng)、Sun JRE 1.8 (64-bit mode)、Eclipse(64-bit mode)、Ant 1.9.

實驗中待測試的程序包括:

1)Euclid:計算兩個整數(shù)之間的差值;

2)WBS:使用整數(shù)和布爾類型輸入來進行更新操作;

3)ArraysCh6、ArraysCh7、ArraysCh8、ArraysCh9、ArraysCh10、ArraysCh11:對數(shù)組進行的基本操作,其中程序名稱后面的6、7、8、9、10、11代表執(zhí)行程序的參數(shù)的個數(shù);

4)Double2Long:將雙精度類型數(shù)據(jù)轉(zhuǎn)換成長整形;CEV4、CEV5、CEV6、CEV7、CEV8、CEV9、CEV10:計算方差,其中程序名稱后面的4、5、6、7、8、9、10代表程序的執(zhí)行個數(shù).

3.2 實驗結(jié)果分析

實驗1.與JDart的對比分析

如表1,總的路徑數(shù)目對于不同數(shù)目節(jié)點是相同的,單節(jié)點的 JDart(動態(tài)符號執(zhí)行)其執(zhí)行時間相比于其它節(jié)點明顯長許多.如ArrayCh9,JDart的執(zhí)行時間是1266323ms,而并行框架不同節(jié)點的運行時間相比其是大幅度減少:2節(jié)點運行時間20607ms,3節(jié)點運行時間為10734ms,如此,隨著節(jié)點數(shù)目的增加,程序執(zhí)行時間在逐漸的縮短.相比JDart,2節(jié)點的執(zhí)行時間相比單節(jié)點節(jié)省了將近62倍,節(jié)點規(guī)模的不斷擴大,該數(shù)字也在不斷增長.

表1 與單節(jié)點符號執(zhí)行(Jdart)的運行時間對比
Table 1 Comparison run time with single node

程序名稱路徑數(shù)不同數(shù)目節(jié)點運行時間/ms單節(jié)點Jdart2節(jié)點3節(jié)點4節(jié)點5節(jié)點6節(jié)點Euclid5015338010481048104810481048WBS13824615350414238397129892799ArraysCh615625906763786061582350424969ArraysCh77812553998100326702597347024523ArraysCh8390625245512150609928822567274515ArraysCh9195312512663232060710734944477086500ArraysCh10#?25963138271030698458625ArraysCh11#?321191622011551102169009CEV465611094385476305504537032400CEV559049140876104768905603149123809CEV653144114065821563210248809565204325CEV7#?20449132211008587476645CEV8#?24082160471292397457566CEV9#?30566241941319498588656CEV10#?355792016911481108719658Double2Long400303310081008100810081008?：代表運行時間長于1h，#：代表路徑條數(shù)大于200萬條

從表1可以看出,JDart的執(zhí)行效率相比于Jdart-parallel有明顯的差距,Jdart-parallel的執(zhí)行效率明顯優(yōu)于JDart.隨著節(jié)點數(shù)目的增加,Jdart-parallel的執(zhí)行效率在不斷的提高,從本質(zhì)上證明了Jdart-parallel并行符號執(zhí)行的優(yōu)勢.

實驗2.節(jié)點規(guī)模對符號執(zhí)行的性能影響

從實驗中可以看出,隨著節(jié)點數(shù)目的不斷增加,程序的執(zhí)行效率在明顯提升,并且隨著節(jié)點數(shù)目的逐漸增多,程序的執(zhí)行效率越高,能更好的體現(xiàn)出并行符號執(zhí)行的優(yōu)勢.此外,隨著節(jié)點數(shù)目的增加,程序的執(zhí)行時間在逐漸的縮短,從執(zhí)行時間上可以對比分析出并行符號執(zhí)行的優(yōu)勢,具體影響如下圖標所示:

本實驗主要對照的是節(jié)點數(shù)目對實驗的影響,擬使用6個實驗節(jié)點來檢測,檢測每個節(jié)點具體運行對實驗結(jié)果的影響,然后對比最初始的程序運行時間,對比判斷出隨著節(jié)點數(shù)目的增多,實驗結(jié)果的最終變化,以此來預(yù)測節(jié)點規(guī)模對實驗的影響.

圖4 不同節(jié)點規(guī)模下的符號執(zhí)行運行時間Fig.4 Symbolic Execution Runtime at Different Node Scales

圖4描述了在Jdart-parallel執(zhí)行工具下,對于待測程序,在不同工作節(jié)點下的執(zhí)行時間,其中對每一個待測程序而言,從左到右節(jié)點數(shù)目在逐漸的增加.從圖中可以看出,對于每一個待測程序,隨著節(jié)點數(shù)目的增加,執(zhí)行時間在逐漸的縮短,對于程序Double2Long和Euclid,由于程序結(jié)構(gòu)比較簡單、規(guī)模較小,所以在執(zhí)行的過程中只用到了其中某一個節(jié)點,因此執(zhí)行時間基本上是相同的.

圖4橫軸表示待測程序的名稱,縱軸表示待測程序的執(zhí)行時間,柱狀圖的高度表示程序的具體執(zhí)行時間,不同的顏色代表不同的節(jié)點數(shù)目執(zhí)行待測程序的時間,圖中可以看出:隨著節(jié)點數(shù)目的增加,執(zhí)行相同待測程序的時間在減少.

圖5和圖6描述了待測程序CEV、Arrays和其變化程序在不同節(jié)點下的運行時間.從圖中可以看出,隨著節(jié)點數(shù)目的不斷增加,每個待測程序的執(zhí)行時間在逐漸的減少,說明了并行符號執(zhí)行的執(zhí)行效率隨著節(jié)點數(shù)目的增加在提升,同時執(zhí)行程序的規(guī)模隨著節(jié)點數(shù)目的增加在增大.

圖7描述了在并行框架下,部分程序的加速比(加速比=單節(jié)點/n節(jié)點,其中n:2,3,4,5,6),隨著節(jié)點數(shù)目的逐漸增加,加速比在逐漸的提升,程序的運行效率在逐漸提升,其中程序Euclid和Double2Long由于程序規(guī)模較小,只使用一個節(jié)點,所以加速比沒變化.

實驗分析:

執(zhí)行時間:隨著程序規(guī)模逐漸增加,Jdart(單節(jié)點)的執(zhí)行時間在逐漸增加,但是Jdart-parallel的執(zhí)行時間相比Jdart執(zhí)行時間明顯減少.Jdart執(zhí)行時間比并行時間多,如表1中單節(jié)點和2 節(jié)點最為明顯,原因是Jdart的執(zhí)行沒使用到多核技術(shù),執(zhí)行的過程中隨著內(nèi)存的逐漸消耗程序會出現(xiàn)卡頓等現(xiàn)象,卡頓期間的時間消耗比較高.并行執(zhí)行時每個節(jié)點都使用較小的路徑樹,占用資源較少,減輕了卡頓現(xiàn)象.

圖5 CVE在不同節(jié)點下運行時間Fig.5 CVE run time at different nodes

圖6 Arrays在不同節(jié)點下運行時間Fig.6 Arrays run time at different nodes

圖7 加速比Fig.7 Speedup ratio

執(zhí)行大規(guī)模程序能力:隨著程序規(guī)模的逐漸增加,Jdart-parallel隨著節(jié)點數(shù)目的增加,程序的執(zhí)行效率在不斷的增強,體現(xiàn)了Jdart-parallel執(zhí)行大規(guī)模程序的能力.

從上述的實驗結(jié)果可以看出,Jdart-parallel并行符號執(zhí)行在執(zhí)行程序方面的優(yōu)勢:首先并行符號執(zhí)行在執(zhí)行程序的過程中相比于非并行執(zhí)行時間明顯縮短;其次是隨著節(jié)點數(shù)目的不斷增多,執(zhí)行相同的程序,并行方式明顯比非并行執(zhí)行能力強;隨著程序規(guī)模的逐漸增加,并行符號執(zhí)行執(zhí)行時間比非并行節(jié)省許多,說明了并行符號執(zhí)行可以執(zhí)行較大規(guī)模程序的能力.

與動態(tài)符號執(zhí)行相比,并行動態(tài)符號執(zhí)行使用多個節(jié)點,在多節(jié)點上分別執(zhí)行路徑探索任務(wù).由以上實驗結(jié)果可以看出,并行動態(tài)符號執(zhí)行工具相比于原來的動態(tài)符號執(zhí)行工具而言測試相同的程序能有效地縮短執(zhí)行時間,并行符號執(zhí)行使用多個節(jié)點測試相應(yīng)程序比原始動態(tài)符號執(zhí)行測試相同的程序提高時間效率,同時加速比在逐漸增加(加速比=單節(jié)點/n節(jié)點,其中n:2,3,4,5,6),實驗結(jié)果證明并行動態(tài)符號執(zhí)行工具Jdart-parallel在提高符號執(zhí)行效率方面具有良好的效果.

4 相關(guān)工作

為了解決并行符號執(zhí)中面臨的效率問題,學術(shù)界提出了一些基于并行技術(shù)的優(yōu)化方法.

ParSym[14]是一種并行動態(tài)符號執(zhí)行,通過一個Symbolic Execution Monitor對整個符號執(zhí)行進行控制和任務(wù)分配,符號執(zhí)行中的每條路徑被當作一個獨立的任務(wù).在符號執(zhí)行中產(chǎn)生的新任務(wù)被動態(tài)地分配到各個節(jié)點進行執(zhí)行.ParSym采用了集中式的任務(wù)調(diào)度方法,涉及到較多的任務(wù)分配和回收等操作,當路徑比較龐大時會耗費較多的通信代價.

靜態(tài)分區(qū)技術(shù)[15]使用一系列的前置條件來對符號執(zhí)行樹進行分區(qū),這樣做的目的是允許我們可以高效的分布執(zhí)行符號執(zhí)行,減少搜索的時間,它們在執(zhí)行的過程中每一個并行實例執(zhí)行各自的運行框架,相互之間很少有交互,節(jié)省時間,但是使用這些先決條件可能使得不同的節(jié)點搜索相同的路徑,搜索的重復率較高,浪費時間,同時靜態(tài)分區(qū)不能實現(xiàn)節(jié)點之間的負載均衡.

Cloud9[16,17]是第一個使用大規(guī)模集群的符號執(zhí)行系統(tǒng)可以線性的擴展許多的節(jié)點,是一個請求式的測試軟件,它主要的功能結(jié)構(gòu)包括工作節(jié)點和負載均衡器,主要依賴均衡器來分配相應(yīng)的搜索任務(wù),并把搜索進行并行化操作,它可以自動化的測試現(xiàn)實世界中的軟件,節(jié)省了很多時間.Cloud9提供了一個系統(tǒng)的寫符號測試的接口,只需要輸入測試數(shù)據(jù)和測試行為,可以提升測試的效率.Cloud9有許多自身的優(yōu)勢:不僅可以處理單線程的程序,還可以處理多線程的程序和分布式系統(tǒng),在多路徑、多任務(wù)同時進行時,Cloud9通過均衡器來實現(xiàn)對于負載的均衡.但是Cloud9在執(zhí)行的過程中需要維護整棵符號執(zhí)行樹,路徑搜索消耗大量多余時間.而本文需要維護的只是個子樹,節(jié)省了存儲空間和搜索時間.此外,Cloud9是針對經(jīng)典的符號執(zhí)行工具而非動態(tài)符號執(zhí)行,在任務(wù)的產(chǎn)生和分配機制上與本文是不同的.

Quoc-Sang Phan等人提出了一種Concurrent Bounded Model Checking(CBMC)方法[18].該方法基于經(jīng)典的符號執(zhí)行工具Symbolic PathFinder進行并行的模型檢測.它首先通過路徑探索,搜索到特定路徑的所有可行路徑,然后將這些路徑進行合并成一個大的約束進行求解.求解時采用并行技術(shù),將各條路徑的約束分配到多個節(jié)點進行求解.該方法只針對的是模型檢測的應(yīng)用場景,只對約束求解過程進行并行,與本文的動態(tài)符號執(zhí)行在應(yīng)用場景和并行模式上是不同的.

5 總 結(jié)

本文基于Actor并行模型,提出了一種并行動態(tài)符號執(zhí)行方法,它實現(xiàn)了兩個層面上的并行.首先可以在多個節(jié)點上并行分析程序的路徑子樹,并通過子樹轉(zhuǎn)移實現(xiàn)動態(tài)的負載均衡.另一方面在節(jié)點內(nèi)部,將約束求解和路徑探索兩項耗時的工作并行,來進一步提高效率.

通過原型工具Jdart-parallel做的相關(guān)對比試驗結(jié)果表明,相比于原來的動態(tài)符號執(zhí)行工具,測試相同的程序,能在時間效率上得到很大提升,證明了并行化符號執(zhí)行在提高效率方面的有效性,同時也體現(xiàn)出并行符號執(zhí)行工具Jdart-parallel在提高符號執(zhí)行效率方面的優(yōu)勢,在處理較大規(guī)模程序中效果也比較明顯.

未來的工作主要考慮能否在約束求解任務(wù)分配支持啟發(fā)式地搜索分配方式,能更加準確快速地搜索到與上一條相似度最高的那條路徑分配,充分利用上一條已保存的求解結(jié)果,可以進一步地提高效率,此外還希望該模型可以支持規(guī)模更大的程序,結(jié)合已有的各種優(yōu)化機制,期望能夠在實際的項目得到應(yīng)用.

[1] Bezier B.Software testing techniques,2nd edition[M].Van Nostrand Reinhold,New York,1990.

[2] King J C.Symbolic execution and program testing[J].Communications ACM,1976,19(7):385-394.

[3] Li Zhou-jun,Zhang Jun-xian,Liao Xiang-ke.Survey of software vulnerabllity detection techniques[J].Journal of Computer,2015,38(4):717-732.

[4] King J C.Symbolic execution and program testing[J].Communications of the Acm,1976,19(7):385-394.

[5] Sen K.DART:directed automated random testing[J].Acm Sigplan Notices,2005,40(6):213-223.

[6] Bucur S,Ureche V,Zamfir C,et al.Parallel symbolic execution for automated real-world software testing[C].Conference on Computer Systems,ACM,2011:183-198.

[7] Phan Q S,Malacaria P,Reanu C S.Concurrent bounded model checking[J].Acm Sigsoft Software Engineering Notes,2015,40(1):1-5.

[8] Kasper Luckow,Marko Dimjasevic,Dimitra Giannako poulou,et al.JDart:a dynamic symbolic analysis framework[C].International Confercence on Tools and Algorithms for the Construction and Analysis of Systems,Springer Berlin Heidelberg,2016:442-459.

[9] Dong Qi-xing,Zeng Fan-ping,Yan Jun.Improve the solving of non-linear arithmetic constraints in dynamic symbolic execution[J].Journal of Chinese Computer System,2014,35(11):2396-2401.

[10] Cadar C,Dunbar D,Engler D.KLEE:unassisted and automatic generation of high-coverage tests for complex systems programs[C].Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation,USE-NIX Association,2008:209-224.

[11] Gupta A.Feedback-directed unit test generation for C /C ++ using concolic execution[C].International Conference on Software Engineering,IEEE,2013:132-141.

[12] Godefroid P,Levin M Y,Molnar D.SAGE:whitebox fuzzing for security testing[J].Queue,2012,10(1):40-44.

[13] An Jing.A research on key technologies of dynamic symbolic[D].Beijing:Beijing University of Posts and Telecommunications,2014.

[14] Siddiqui J H,Khurshid S.ParSym:parallel symbolic execution[C].International Conference on Software Technology and Engineering,2010:V1-405-V1-409.

[15] Staats M,Pǎsǎreanu C.Parallel symbolic execution for structural test generation[C].Nineteenth International Symposium on Software Testing and Analysis,ISSTA 2010,Trento,Italy,2010:183-194.

[16] Ciortea L,Zamfir C,Bucur S,et al.Cloud9:a software testing service.[J].Acm Sigops Operating Systems Review,2009,43(4):5-10.

[17] Bucur S,Ureche V,Zamfir C,et al.Parallel symbolic execution for automated real-world software testing [C].Conference on Computer Systems,ACM,2011:183-198.

[18] Phan Q S,Malacaria P,Reanu C S.Concurrent bounded model checking[J].Acm Sigsoft Software Engineering Notes,2015,40(1):1-5.

[19] Cassar I,Francalanza A.On implementing a monitor oriented programming framework for actor systems[J].Lecture Notes in Computer Science,2016.

附中文參考文獻：

[3] 李舟軍,張俊賢,廖湘科,等.軟件安全漏洞檢測技術(shù)[J].計算機學報,2015,38(4):717-732.

[10] 董齊興,曾凡平,嚴 俊,等.改進動態(tài)符號執(zhí)行中的非線性約束求解過程[J].小型微型計算機系統(tǒng),2014,35(11):2396-2401.

[12] 安 靖.動態(tài)符號執(zhí)行關(guān)鍵技術(shù)研究[D].北京:北京郵電大學,2014.