基于模型檢測(cè)的類測(cè)試自動(dòng)生成技術(shù)研究.pdf

1、高可信軟件技術(shù)是軟件理論研究和工程實(shí)踐領(lǐng)域關(guān)注的焦點(diǎn)之一。近年來(lái)，越來(lái)越多的形式化方法被應(yīng)用于提高軟件質(zhì)量的研究上。軟件測(cè)試是保證軟件產(chǎn)品可靠性和正確性的有效手段之一，而模型檢測(cè)是一種確保設(shè)計(jì)規(guī)范正確性的形式化自動(dòng)驗(yàn)證技術(shù)。研究發(fā)現(xiàn)，模型檢測(cè)中生成的反例可有效應(yīng)用于測(cè)試用例的生成，顯著減少測(cè)試代價(jià)，提高軟件質(zhì)量。本文主要研究基于模型檢測(cè)的類測(cè)試自動(dòng)生成技術(shù)。 本文分別采用數(shù)據(jù)流測(cè)試和變異測(cè)試的方法，并結(jié)合模型檢測(cè)器Java．Pa

2、thFinder(JPF)，將測(cè)試生成問(wèn)題簡(jiǎn)化成模型檢測(cè)中尋找反例的問(wèn)題，提出了兩種面向?qū)ο筌浖y(cè)試用例自動(dòng)生成的方法。 首先采用數(shù)據(jù)流測(cè)試的方法，通過(guò)設(shè)置陷阱性質(zhì)，用時(shí)序邏輯公式表示數(shù)據(jù)流測(cè)試的覆蓋準(zhǔn)則，提出一種自動(dòng)生成測(cè)試用例的方法，并在JPF上實(shí)現(xiàn)。該方法滿足數(shù)據(jù)流覆蓋準(zhǔn)則，適用于Java類內(nèi)方法間調(diào)用序列的測(cè)試。算法分析與實(shí)驗(yàn)結(jié)果表明，通過(guò)設(shè)置適當(dāng)?shù)乃阉魃疃?，本文提出的算法使得類?shù)據(jù)流測(cè)試的覆蓋率提高了8％，并能發(fā)現(xiàn)隱藏

3、在程序當(dāng)中的錯(cuò)誤；通過(guò)本文提出的方法調(diào)用選擇原則，可顯著減少生成調(diào)用序列的長(zhǎng)度；與JPF的DFS算法相比，本文提出的算法減少了搜索過(guò)程中產(chǎn)生的冗余狀態(tài)，并及時(shí)進(jìn)行了回退，在內(nèi)存消耗基本相同的情況下本文算法生成的新?tīng)顟B(tài)數(shù)減少了65％，回退次數(shù)減少了90％，處理的狀態(tài)數(shù)減少了88％，算法的執(zhí)行時(shí)間也減少了28％，有效減少了測(cè)試生成的代價(jià)。此外，基于變異測(cè)試的思想，采用類復(fù)制的方法，應(yīng)用JPF來(lái)保證軟件執(zhí)行過(guò)程中產(chǎn)生的錯(cuò)誤在輸出結(jié)果中可見(jiàn)，自

4、動(dòng)生成滿足變異覆蓋準(zhǔn)則的測(cè)試用例，適用于類之間方法調(diào)用的測(cè)試，從而實(shí)現(xiàn)了Java類之間的測(cè)試用例自動(dòng)生成。算法分析與實(shí)驗(yàn)結(jié)果表明，針對(duì)TreeMap類的測(cè)試用例生成實(shí)驗(yàn)，本文提出的方法覆蓋了其中主要的面向?qū)ο筇匦?，且生成的變異?shù)多達(dá)211個(gè)，而反例數(shù)僅26個(gè)就覆蓋了100％的有效變異，顯著減少了測(cè)試生成的代價(jià)；與Visser提出的模型檢測(cè)器JPF上的符號(hào)執(zhí)行方法相比，在對(duì)TrreeMap類中的deleteEntry、fixAfterDe