基于模型檢驗的測試用例生成技術(shù)研究.pdf

1、軟件測試是保證軟件產(chǎn)品可靠性和正確性的有效方法，其中設(shè)計和生成有效的測試用例是決定測試質(zhì)量的重要因素之一，而測試用例自動生成可以節(jié)省測試時間，降低開發(fā)成本。模型檢驗是確保軟件設(shè)計正確性的形式化驗證技術(shù)。給出系統(tǒng)有限狀態(tài)模型和性質(zhì)的邏輯表達(dá)，模型檢驗?zāi)茏詣訖z驗該性質(zhì)在這個模型上是否成立，特別是當(dāng)某條時序邏輯公式不成立時，能夠自動地拋出一條執(zhí)行路徑來表明系統(tǒng)并不滿足這條性質(zhì)，稱這條路徑為反例。模型檢驗工具自動生成反例的功能，可以用于實現(xiàn)測試

2、用例生成自動化。近年來，人們對使用模型檢驗自動生成測試用例進行了研究，使之在變異測試、結(jié)構(gòu)化測試、數(shù)據(jù)流測試、類測試方面得到應(yīng)用。 本文在已有工作基礎(chǔ)上，總結(jié)歸納了模型檢驗技術(shù)用于測試用例生成的若干種方法框架，完善了基于模型檢驗生成數(shù)據(jù)流測試用例的方法，提出了一種基于模型檢驗的類測試用例生成方法。論文主要工作包括： (1)使用時序邏輯描述結(jié)構(gòu)化覆蓋標(biāo)準(zhǔn)，并證明了時序邏輯描述與相應(yīng)覆蓋標(biāo)準(zhǔn)的等價性； (2)提出一種