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

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