基于形式規(guī)格說(shuō)明的類(lèi)測(cè)試框架研究.pdf

1、面向?qū)ο蠹夹g(shù)作為一種全新的軟件工程思想，在軟件開(kāi)發(fā)中的廣泛使用。但是其獨(dú)有的封裝、繼承、多態(tài)等特性，使得傳統(tǒng)的軟件測(cè)試技術(shù)已經(jīng)不能夠有效地完成測(cè)試。因此測(cè)試策略和測(cè)試方法都需要進(jìn)行相應(yīng)的改進(jìn)。 形式化方法是基于數(shù)學(xué)方法來(lái)描述目標(biāo)軟件系統(tǒng)性質(zhì)的軟件開(kāi)發(fā)方法，它為系統(tǒng)說(shuō)明、開(kāi)發(fā)和驗(yàn)證提供了一個(gè)框架。Object-Z是一種形式規(guī)格說(shuō)明語(yǔ)言，其基礎(chǔ)是Z語(yǔ)言。用Obiect-Z來(lái)描述面向?qū)ο筌浖?guī)格說(shuō)明，具有簡(jiǎn)明、精確、無(wú)二義性的優(yōu)點(diǎn)。

2、 Harrold和Rothermel將類(lèi)的單元測(cè)試分成三個(gè)級(jí)別：方法內(nèi)測(cè)試、方法間測(cè)試和類(lèi)內(nèi)部測(cè)試。Stock和Carrington提出的基于形式化規(guī)格說(shuō)明的測(cè)試模板框架TTF(Test Template Framework)，可以在詳細(xì)設(shè)計(jì)階段就生成類(lèi)測(cè)試用例，但生成的測(cè)試模板只能完成方法內(nèi)和方法間測(cè)試，而無(wú)法判斷測(cè)試模板序列執(zhí)行后，類(lèi)內(nèi)部狀態(tài)的正確性，即無(wú)法完成類(lèi)內(nèi)部測(cè)試。 本文提出的基于形式規(guī)格說(shuō)明的類(lèi)測(cè)試框架是針對(duì)

3、TIT框架在類(lèi)狀態(tài)測(cè)試方面的擴(kuò)展。主要思想：首先，利用TTF框架生成的方法測(cè)試模板構(gòu)造類(lèi)的有限狀態(tài)自動(dòng)機(jī)。其中，構(gòu)造過(guò)程分為狀態(tài)推導(dǎo)和遷移規(guī)則推導(dǎo)兩個(gè)步驟；然后，生成測(cè)試模板所有可能的調(diào)用序列，即測(cè)試路徑生成；最后，根據(jù)測(cè)試路徑構(gòu)造測(cè)試類(lèi)的集合，每個(gè)測(cè)試類(lèi)是一個(gè)Obiect-Z描述的類(lèi)模式。 擴(kuò)展后的ETTF框架不僅可以完成對(duì)類(lèi)內(nèi)部方法的測(cè)試，并且可以考察類(lèi)內(nèi)部狀態(tài)改變的正確性，達(dá)到完整的單元測(cè)試的目的。同時(shí)，由于測(cè)試用例是從O