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

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

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

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

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