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

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

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

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