基于模型檢測多反例對軟件進(jìn)行調(diào)試.pdf

1、如今，模型檢測已經(jīng)普遍應(yīng)用于對軟件屬性的檢測中。模型檢測技術(shù)含有高度的自動化性，當(dāng)設(shè)計的系統(tǒng)違背規(guī)約時，模型檢測器會返回一個源碼級別的錯誤路徑即反例，反例中包含了對應(yīng)于違背規(guī)約的錯誤解釋信息。通過對反例中的解釋信息進(jìn)行分析，我們可以得到系統(tǒng)為什么違背系統(tǒng)屬性的錯誤原因，而這些分析將會給系統(tǒng)修復(fù)過程提供了重要的依據(jù)。
　　鑒于模型檢測的諸多優(yōu)點(diǎn)，在故障定位技術(shù)中應(yīng)用模型檢測技術(shù)已經(jīng)成為一個研究熱點(diǎn)。然而，復(fù)雜系統(tǒng)的反例往往顯得非常的

2、冗余和復(fù)雜，甚至讓人覺得難以理解，這就使得我們需要花費(fèi)大量時間來檢查反例進(jìn)而找出引發(fā)系統(tǒng)錯誤的起因?，F(xiàn)在的模型檢測器已經(jīng)可以產(chǎn)生所有的反例，所以我們更希望能夠利用多反例來查找系統(tǒng)中故障的位置，而不是只采用一個反例的信息。本文提出了距離度量技術(shù)和Tarantula技術(shù)在錯誤解釋和故障定位上的拓展。
　　在以往的方法中，尋找故障用的是單反例，對于反例的選擇也是沒有依據(jù)的隨意之舉，通常會導(dǎo)致這個反例在故障定位中并不是一個好的選擇。已知單

3、獨(dú)的反例在調(diào)試中可能對找出錯誤沒有幫助，那些僅僅采用一個單獨(dú)反例會由于信息的不確定性，在不斷地嘗試不同的反例中浪費(fèi)大量時間，而多反例會給出清楚的線索來進(jìn)行故障定位。在本文方法中，根據(jù)反例和成功執(zhí)行路徑集合以及利用距離度量技術(shù)和Tarantula技術(shù)，可以找出一個反例和它的最優(yōu)路徑。這個反例就是一個最佳選擇，能夠很好地讓我們在特定信息線索中找出含有故障的謂詞，再通過與最優(yōu)路徑對比就可以找出引起故障產(chǎn)生的原因。在Tarantula技術(shù)中，會

4、提供一個在代碼中聲明可能成為故障的懷疑度高低的排名，這類信息就是找到基準(zhǔn)反例的根據(jù)。
　　通常，在代碼太多時會難以找出故障的位置，因而我們提出了一個在部分可疑代碼中，基于距離度量分析對比進(jìn)行故障定位的方法。對整個路徑中代碼的部分壓縮區(qū)域進(jìn)行分析可以提高效率和精確性。距離度量提供了尋找最優(yōu)成功執(zhí)行路徑的技術(shù)，它是對應(yīng)于反例來選擇的。我們將這兩種技術(shù)融合在一起，從而加快了找錯的能力，同時，這種融合也更利于精確度上的提高。當(dāng)然，最后我們