基于形式規(guī)格說明的類測試框架研究.pdf

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

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

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