基于Z規(guī)格說明的測試用例自動生成和評估.pdf

1、軟件測試是軟件質(zhì)量保證的重要手段,并且代表了規(guī)格說明、設計和編碼的最終評審.測試用例的生成是軟件測試的關鍵和難點.目前,在手工生成測試用例的情況下,要求軟件測試人員具有一定的經(jīng)驗和較高的專業(yè)水平,并且測試人員很難檢測到不熟悉的錯誤,軟件質(zhì)量存在不穩(wěn)定性.因此,有必要開發(fā)測試工具,尤其是支持測試用例自動生成的工具,以提高測試效率.測試過程自動化的關鍵是測試用例的自動生成.測試用例自動生成減少測試人員的勞動,提高測試效率,更好地保證了軟件的

2、質(zhì)量.在自動生成測試用例時,測試方法和測試充分性標準的選擇將直接影響測試用例的生成.選擇測試充分性準則對軟件的測試是至關重要的,影響著測試的開銷及通過測試的軟件質(zhì)量.形式方法是基于數(shù)學方法來描述目標軟件系統(tǒng)性質(zhì)的軟件開發(fā)方法,它為系統(tǒng)的說明、開發(fā)和驗證提供了一個框架,形式化的規(guī)格說明有利于測試的自動化.Z語言是目前比較流行、使用較為成功而有效的語言,它是基于模型的形式化規(guī)格語言,具有精確、簡潔、無二義性的特點,有利于開發(fā)高質(zhì)量的程序.本

3、文在Paul Ammann和Jeff Offutt提出用范疇劃分方法產(chǎn)生測試框架的基礎上,探討了從Z規(guī)格說明推導出測試用例的過程、方法和技術.本文的主要工作是:按照范疇劃分測試中的三個測試充分性準則All-Combination、Each-Choice-Used和Base-Choice-Coverage先產(chǎn)生測試框架.接下來,為實例化測試框架引入了線性規(guī)劃模型,把測試框架線性化為一些線性不等式組,利用這些不等式組構造線性規(guī)劃模型,并利用

4、線性規(guī)劃程序的編程接口LINDOAPI解出不等式組,實例化測試框架.為了構造線性規(guī)劃模型,本文對Paul Ammann和Jeff Offutt提出的產(chǎn)生測試框架的步驟進行了改進,增加了測試框架線性化的步驟.本文還較好地解決了實例化測試框架時,判斷測試框架是否可行的問題.本文的另一個工作是對按All-Combination、Each-Choice-Used和Base-Choice-Coverage三個測試充分性標準產(chǎn)生的測試用例在揭錯能力