基于Object-Z規(guī)格說明的測試用例生成方法研究.pdf

1、隨著信息技術(shù)的發(fā)展，軟件規(guī)模不斷擴(kuò)大，而且越來越復(fù)雜，如何保證和提高軟件質(zhì)量成為軟件界最為關(guān)心的問題之一。軟件測試作為保證軟件質(zhì)量的關(guān)鍵技術(shù)，能夠有效地發(fā)現(xiàn)軟件中的故障。對于某些安全關(guān)鍵的軟件，其測試費(fèi)用是所有其它軟件工程階段費(fèi)用總和的三到五倍。因而，提高軟件測試的有效性和測試效率、降低軟件開發(fā)成本己成為軟件工程師迫切需要解決的任務(wù)之一。 測試用例的好壞直接影響軟件測試的效果。根據(jù)測試用例產(chǎn)生的依據(jù)可以將軟件測試分為白盒測試和黑

2、盒測試，從規(guī)格說明產(chǎn)生測試用例的方法稱為黑盒測試。形式的軟件規(guī)格說明具有精確的符號表示和清晰的語義，能夠進(jìn)行推理和證明，同時也便于工具的處理。因此，用形式的規(guī)格說明作為測試用例的來源將會使得測試用例的自動構(gòu)造成為可能。 目前基于Object-Z的形式規(guī)格說明構(gòu)造測試用例的研究主要集中在理論研究階段，測試用例的自動生成幾乎沒有相應(yīng)的工具支持，這主要是因?yàn)镺biect-Z是基于數(shù)學(xué)和邏輯的語言，比較難以提取其中表達(dá)式的語義，這就難以

3、自動產(chǎn)生測試用例。本文研究從Object-Z規(guī)格說明產(chǎn)生測試用例的自動化過程，這一過程主要包含三個階段：Object-Z語言的自動解析、語義自動抽取和測試用例自動產(chǎn)生。 本文針對操作模式中使用的調(diào)用模式提出了產(chǎn)生測試用例的方法和若干測試準(zhǔn)則，該方法能夠驗(yàn)證代碼中的函數(shù)是否正確地調(diào)用了其他類的函數(shù)。 本文對Object-Z語言的部分文法進(jìn)行了改進(jìn)，以減少自動解析時的沖突，提出并完善了用于從Object-Z圖形與數(shù)學(xué)符號結(jié)合

4、的語言轉(zhuǎn)換成易于計(jì)算機(jī)處理的純文本LaTeX語言的方法，并構(gòu)造了相應(yīng)的文法來解析用Object-Z編寫的規(guī)格說明，生成語法樹，根據(jù)語法樹可以提取出相關(guān)語義。為了人們方便地編寫和閱讀規(guī)格說明，Object-Z語言使用了大量的模式復(fù)合和簡寫形式，這給計(jì)算機(jī)提取完整語義自動產(chǎn)生測試用例造成了困難，因此本文還給出了還原完整語義的方法。 本文實(shí)現(xiàn)了提取規(guī)格說明中操作模式前置條件的方法，并分離出文字集及它們之間的邏輯關(guān)系。本文實(shí)現(xiàn)了產(chǎn)生符合