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

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

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

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