摘 要：軟件測試數(shù)據(jù)生成在軟件系統(tǒng)開發(fā)費(fèi)用中占很大比重。如果該過程能自動實(shí)現(xiàn)，則會極大地減少軟件開發(fā)的周期和費(fèi)用。測試用例的生成工作包含選定被測任務(wù)、分析輸入數(shù)據(jù)、確定其取值并分析對應(yīng)的輸出數(shù)據(jù)。其中分析對應(yīng)的輸出數(shù)據(jù)是決定測試是否成功的關(guān)鍵環(huán)節(jié)。測試用例選取的一個中心原則，就是以用最少的測試用例找到盡可能多的錯誤。目前的工具尚不能完成自動生成測試用例這個環(huán)節(jié)，往往是只能采用人工選取的方法。按所采用的方法和研究對象的不同，將測試用例自動生成方法主要分為5類：基于有限狀態(tài)集的測試，基于標(biāo)注的轉(zhuǎn)換系統(tǒng)的測試，針對面向模型的需求規(guī)格說明的測試，針對面向?qū)ο筌浖臏y試，以及運(yùn)用模型檢查生成測試用例的方法。在簡單介紹前4種方法之后，重點(diǎn)對模型檢查的方法進(jìn)行詳細(xì)的分析和探討。

關(guān)鍵詞：測試用例；自動生成；模型檢查；形式化建模

中圖分類號：TP311 文獻(xiàn)標(biāo)識碼：A

文章編號：1004-373X(2008)06-126-04

Research on Status ofAutomated Test Case Generation Method

MA Liang，ZHANG Gang

(China Aerospace Engineering Consultation Center，Beijing，100037，China)

Abstract：It costs much money that software test data generation in software development.If this process can realize automatically，it will reduce period and money a lot in software development. Test case generation includes of choosing the object tested，analyzing the data input，making sure the value of the data and analyzing the relevant data output.It is key of analyzing the relevant data output that decides whether test is successful or not.The central principle of choosing test case is that it can find more error using less of test case.At present，there are few tools that can generate test case automated completely.Now，people always do it man-made.Based on the difference of the methods and object researched，it has five methods of automatically testing case generation.It includes that test based on finite state，test of transformation system based on label，test aiming at model-oriented requirement specifications，test aiming at object-oriented software and method of automated test case generation by model checking.After some brief introduction of the four methods before，it gives more information about the method of model checking here.

Keywords：test case；automated generation；model checking；form modeling

通過對目前測試用例自動生成方法的研究現(xiàn)狀進(jìn)行調(diào)研，國外的一些機(jī)構(gòu)和組織在測試用例自動生成方法這一領(lǐng)域已經(jīng)開展了大量的研究工作，例如美國國家標(biāo)準(zhǔn)局(NIST)，并取得了階段性的研究成果，有些研究組織正努力將測試用例自動生成方法運(yùn)用于實(shí)踐中。目前國內(nèi)對自動生成測試用例方法的研究還處于起步階段，與國外相比，存在一定的差距。國內(nèi)一些高校和研究機(jī)構(gòu)，例如，國防科技大學(xué)、南京大學(xué)、中科院軟件所，正在進(jìn)行利用形式化方法進(jìn)行安全性保障的單元技術(shù)研究。

在軟件領(lǐng)域，形式化方法最初用于對高可靠性軟件進(jìn)行形式化驗(yàn)證，由于其在驗(yàn)證軟件特性時可生成反例的特點(diǎn)，逐漸被用于測試用例的生成中。模型檢查技術(shù)是目前形式化方法在實(shí)際運(yùn)用中的常用形式，基于需求的運(yùn)用模型檢查自動生成測試用例的研究已廣泛開展。本文將針對運(yùn)用模型檢查生成測試用例的方法的優(yōu)缺點(diǎn)及其原理，主要技術(shù)途徑進(jìn)行著重的介紹和分析。

1 特定領(lǐng)域生成測試用例方法現(xiàn)狀

測試用例的設(shè)計和編制是軟件測試中最重要的活動。測試用例是測試工作的指導(dǎo)，能有效地保障軟件測試的質(zhì)量，也是評估測試結(jié)果的度量基準(zhǔn)。目前的測試用例設(shè)計的手段主要以手工方式為主，已有一些關(guān)于測試用例自動生成方法的研究。在運(yùn)用手工方式設(shè)計測試用例時，存在測試用例的設(shè)計過程不規(guī)范的問題。同時，設(shè)計的用例的輸出結(jié)果的正確性(即根據(jù)測試輸入數(shù)據(jù)得到測試的輸出數(shù)據(jù))還需要通過人工結(jié)合需求進(jìn)行判定來保證。

由于軟件的復(fù)雜性，以目前的測試技術(shù)水平發(fā)現(xiàn)軟件中的所有錯誤是不可能的，而且軟件錯誤在所難免，如何提高對軟件進(jìn)行測試的充分性是目前要解決的一個問題。

目前正在研究的主要幾種類型的方法有：

(1) 基于有限狀態(tài)機(jī)的測試；

(2) 基于標(biāo)注的轉(zhuǎn)換系統(tǒng)(LTS)的測試；

(3) 針對面向模型的需求的測試；

(4) 針對面向?qū)ο筌浖臏y試；

(5) 運(yùn)用模型檢查的測試。

以上的一些方法已有與之對應(yīng)的原型工具，有些已經(jīng)投入到實(shí)驗(yàn)中，另外，當(dāng)前已有一些商業(yè)化的測試輔助工具，支持自動生成測試用例的功能。在以上5種測試用例自動生成方法中，除模型檢查方法之外，其他4種方法主要適用于特定的應(yīng)用領(lǐng)域?；谀Ｐ蜋z查的測試用例生成方法是目前被廣泛研究的一種確認(rèn)測試用例生成方法，已有一些階段性的研究成果。

1.1 基于有限狀態(tài)機(jī)的測試

對有限狀態(tài)機(jī)(FSM)的測試是一個廣為人知的研究課題，可以追溯到E.F.Moore 的早期研究：“順序機(jī)的想象實(shí)驗(yàn)”。但此方法的實(shí)際應(yīng)用則是在方法提出很久以后，主要應(yīng)用于對協(xié)議的一致性測試。通常以有限狀態(tài)語言定義有限狀態(tài)機(jī)中的狀態(tài)以及狀態(tài)的有限集合的值，并對有限狀態(tài)機(jī)中的狀態(tài)遷移加以描述。其測試方法是：給定一個需求狀態(tài)機(jī)A的全部信息(狀態(tài)遷移圖或狀態(tài)表格)和一個針對需求的實(shí)現(xiàn)的狀態(tài)機(jī)B，通過將測試序列應(yīng)用到B，觀察輸出結(jié)果，檢驗(yàn)B是否是A的正確實(shí)現(xiàn)^[1]。

基于有限狀態(tài)機(jī)的測試的應(yīng)用的領(lǐng)域較小，但其思想常體現(xiàn)在需求描述和形式化建模中，針對需求的描述方法中就有狀態(tài)圖描述法。實(shí)際上，根據(jù)需求建立的形式化模型可以看作一個有限狀態(tài)機(jī)。

1.2 基于標(biāo)注的轉(zhuǎn)換系統(tǒng)的測試

標(biāo)注的轉(zhuǎn)換系統(tǒng)(LTS)主要用于描述以特定的需求規(guī)格說明語言定義的系統(tǒng)行為，例如，程序代數(shù)(如LOTOS)是一種語義模型為LTS的運(yùn)用廣泛的語言。一個標(biāo)注的轉(zhuǎn)換系統(tǒng)(LTS模型)包括狀態(tài)和狀態(tài)之間的標(biāo)注的狀態(tài)遷移，以狀態(tài)模擬系統(tǒng)的狀態(tài)，以狀態(tài)遷移對系統(tǒng)與系統(tǒng)周圍的環(huán)境發(fā)生的交互進(jìn)行模擬。LTS模型通常以圖或樹的形式描述系統(tǒng)行為以及改變系統(tǒng)狀態(tài)的事件，其中邊被標(biāo)注為事件，代表狀態(tài)遷移，而節(jié)點(diǎn)代表狀態(tài)。針對LTS系統(tǒng)，已開發(fā)出許多測試工具，這些測試工具都是基于ioco測試?yán)碚摚渲幸粋€比較著名的工具是TorX^[2]。

基于標(biāo)注的轉(zhuǎn)換系統(tǒng)的測試的思想與基于有限狀態(tài)機(jī)的測試的思想類似，將系統(tǒng)看作一個有限狀態(tài)機(jī)，系統(tǒng)由狀態(tài)和狀態(tài)遷移組成，由于此方法主要應(yīng)用于以特定的需求規(guī)格語言(如程序代數(shù))定義的系統(tǒng)，比較緊密的結(jié)合這些特定的需求規(guī)格語言的特性，不具有通用性，應(yīng)用到常用的需求中存在難度。

1.3 針對面向模型的需求規(guī)格說明的測試

面向模型的語言，如VDM-SL，Z，B通過描述系統(tǒng)的狀態(tài)，以及改變狀態(tài)的動作建立行為模型。通常用集合、序列、關(guān)系，以及函數(shù)來描述系統(tǒng)中存在的狀態(tài)，而以前置條件，后置條件的形式定義的語法來描述系統(tǒng)的動作。

這種類型的測試方法主要有BZ-TT方法，其他一些相應(yīng)的方法主要有基于Z語言的方法，基于VDM-SL的方法。在其他一些提出的解決方案中，將轉(zhuǎn)換包含到了邏輯設(shè)計模型中，如Prolog，其優(yōu)點(diǎn)在于不需要通過設(shè)計特定的解決方案生成測試用例，由語言本身的特性來實(shí)現(xiàn)測試用例的生成^[3]。這種方法目前還處于理論研究階段，在實(shí)際中的運(yùn)用很少。

1.4 針對面向?qū)ο筌浖臏y試

目前大多數(shù)的軟件系統(tǒng)采用傳統(tǒng)的結(jié)構(gòu)化方法進(jìn)行設(shè)計，即面向結(jié)構(gòu)的軟件，例如目前的航天型號軟件，基本都是通過結(jié)構(gòu)化方法進(jìn)行設(shè)計開發(fā)，很少采用面向?qū)ο蠓椒ㄟM(jìn)行設(shè)計和開發(fā)。目前在軟件開發(fā)領(lǐng)域，面向?qū)ο蠓椒ㄒ驯粡V泛接受與運(yùn)用，出現(xiàn)了大量的運(yùn)用面向?qū)ο蠓椒ㄩ_發(fā)的軟件。測試面向?qū)ο蟮某绦蚝蜏y試結(jié)構(gòu)化方法設(shè)計出的程序有很大的差異，因?yàn)?，在一種環(huán)境下某一個被充分測試的面向?qū)ο蠼M建在任何其他的環(huán)境中不一定意味著其已經(jīng)被充分的測試到。因此，出現(xiàn)了許多特定的針對面向?qū)ο筌浖M(jìn)行測試的研究。

目前此領(lǐng)域的研究進(jìn)展如下：OZTest是針對面向?qū)ο蟪绦虻陌胱詣拥纳蓽y試用例的框架，以O(shè)bject-Z作為形式化的需求規(guī)格說明語言。Object-Z是一種基于模型的面向?qū)ο蟮恼Z言。

由于目前的航天型號軟件基本上采用結(jié)構(gòu)化方法進(jìn)行設(shè)計開發(fā)，因此針對面向?qū)ο筌浖臏y試目前不適合應(yīng)用于航天型號軟件測試。隨著技術(shù)的發(fā)展，面向?qū)ο蠓椒赡軙缓教煨吞栜浖捎?，則可以采用此方法對型號軟件進(jìn)行測試^[4]。

相對于運(yùn)用模型檢查生成測試用例的方法，以上4種方法主要適用于特定的應(yīng)用領(lǐng)域，不具有通用性。

2 運(yùn)用模型檢查生成測試用例方法

在軟件領(lǐng)域，形式化方法最初用于對可靠性要求較高的軟件進(jìn)行需求描述和形式化驗(yàn)證，隨著研究的深入開展，形式化方法的應(yīng)用范圍逐漸擴(kuò)大到軟件的開發(fā)設(shè)計，系統(tǒng)的安全特性驗(yàn)證。模型檢查技術(shù)是一種基于狀態(tài)探測的得到廣泛運(yùn)用的形式化方法，如圖1所示，模型檢查器檢查需求中某個系統(tǒng)特性是否成立時，根據(jù)反映需求的形式化模型在內(nèi)存中構(gòu)造一個有限狀態(tài)轉(zhuǎn)換模型，探測模型的可達(dá)狀態(tài)空間，以檢測被驗(yàn)證的系統(tǒng)特性 (以時序邏輯進(jìn)行描述)與模型是否存在沖突，從而驗(yàn)證這個系統(tǒng)特性對于需求是否成立。當(dāng)被檢驗(yàn)的系統(tǒng)特性與模型存在沖突時，模型檢查器會產(chǎn)生一個反例，證明沖突如何發(fā)生。反例以輸入/輸出序列的形式給出，將有限狀態(tài)轉(zhuǎn)換模型從初始狀態(tài)引入到?jīng)_突發(fā)生的狀態(tài)。

2.1 運(yùn)用模型檢查生成測試用例的原理

因具有在驗(yàn)證系統(tǒng)特性時可產(chǎn)生反例的特點(diǎn)，模型檢查技術(shù)被人們所關(guān)注，作為生成測試用例的引擎。

模型檢查技術(shù)采用特定的形式化建模語言，如SMV，PROMELA，對軟件需求進(jìn)行形式化建模，建立的形式化模型是模型檢查器處理的對象，包括2部分：

(1) 由變量，變量的初始值，描述變量在一定的條件下其值發(fā)生變化的規(guī)則3者有機(jī)組成的有限狀態(tài)模型；

(2) 反映系統(tǒng)特性的時序邏輯。

軟件的功能性需求通常具備如下特征：功能的輸入條件，功能的處理過程，以及相應(yīng)的功能輸出。在運(yùn)用形式化語言描述軟件需求時，首先抽取功能需求涉及到的數(shù)據(jù)，分析數(shù)據(jù)之間的關(guān)系，定義數(shù)據(jù)在各種條件下確定的變換規(guī)則。通過以上建模步驟，軟件的需求被映射為如下模型：變量集合，以及反映變量在確定的輸入條件下產(chǎn)生確定輸出規(guī)則構(gòu)成的需求有限狀態(tài)模型。因此，可由3部分構(gòu)成對變量變換規(guī)則的形式化定義：變量的當(dāng)前值，發(fā)生變換的輸入條件，變量變換后的輸出結(jié)果。

通過對測試目標(biāo)進(jìn)行形式化描述，作為被模型檢查器檢查的驗(yàn)證目標(biāo)，可以由模型檢查器推導(dǎo)出測試用例，例如，驗(yàn)證變量VAR的值從當(dāng)前值A(chǔ)變?yōu)锽(發(fā)生變換的輸入條件為C)。可以運(yùn)用時序邏輯語法描述這個場景(對應(yīng)的測試用例將會測試到這個變換)：測試輸入序列將模型引入到某一狀態(tài)下，使模型中變量VAR的值為A，在此狀態(tài)下，當(dāng)輸入條件C滿足時，則模型的下一狀態(tài)中，模型中變量VAR的值為B。以上是模型檢查中常用的描述測試目標(biāo)的邏輯表達(dá)形式(如以CTL語法對測試目標(biāo)進(jìn)行描述)。通過對描述測試目標(biāo)的CTL進(jìn)行取反，并運(yùn)用模型檢查對其驗(yàn)證，即可將模型引入所關(guān)注的場景，模型檢查就會搜尋到一個反例證明測試目標(biāo)實(shí)際上是成立的，這樣的反例即構(gòu)成了一個測試用例，他將遍歷到所關(guān)注的輸入輸出變換規(guī)則^[5]。

通過對形式化模型中的每個變量的所有變換規(guī)則以時序邏輯語法進(jìn)行定義，并對其進(jìn)行如上取反處理，運(yùn)用模型檢查器驗(yàn)證取反的時序邏輯，自動產(chǎn)生測試序列，就可以覆蓋模型中的變量的輸入輸出變換規(guī)則。此方法已作為從各種形式化語言描述的需求中生成測試用例的基本途徑，如圖2所示。

2.2 主要技術(shù)途徑

運(yùn)用模型檢查生成測試用例的技術(shù)途徑主要有2種：基于運(yùn)算符變異的技術(shù)；通過構(gòu)造陷阱特性結(jié)合模型檢查的方法，以下分別介紹。

2.2.1 基于運(yùn)算符變異的技術(shù)

基于運(yùn)算符變異的思想的理論基礎(chǔ)是耦合效應(yīng)猜想，即在測試中，存在這樣一種現(xiàn)象：能檢測出簡單錯誤的測試用例有可能同時檢測出復(fù)雜的錯誤。其方法是運(yùn)用變異運(yùn)算符對系統(tǒng)的描述進(jìn)行小的改變，例如，對變量的改變。

變異測試的思想已經(jīng)被借鑒到基于需求的測試中：首先定義一套變異運(yùn)算符，這些變異運(yùn)算符針對需求建立的形式化模型或系統(tǒng)特性進(jìn)行小的改變。在文獻(xiàn)[6]的覆蓋分析中，介紹了這種運(yùn)算符變異方法，在文獻(xiàn)[7]中，首次提出了將變異運(yùn)算符運(yùn)用到測試用例生成中，并提出了一種簡單的度量方法，通過檢查整個變異的需求集合中測試用例命中的變異的需求來計算測試用例集合的變異充分性水平，以對測試用例集進(jìn)行評估。

在變異方法針對系統(tǒng)特性進(jìn)行語法上的變異時，往往變異出大量的系統(tǒng)特性，并生成大量的反例，不具有可控性。

2.2.2 通過構(gòu)造陷阱特性結(jié)合

Gargantini和 Heitmeyer，通過構(gòu)造陷阱特性達(dá)到對SCR需求規(guī)格說明的分支覆蓋，并提出一般情況下無法獲得充分的系統(tǒng)特性集合這一觀點(diǎn)：即使可以獲得大量的用于生成測試用例的系統(tǒng)特性，也不能保證其完全覆蓋所有可能的系統(tǒng)行為。因此，SCR需求規(guī)格說明首先轉(zhuǎn)換為模型檢查器的輸入，針對所有分支以不同的標(biāo)記進(jìn)行重新修改，成為新的輸入。然后，針對每個分支構(gòu)造一個陷阱特性。通過以上步驟，生成的測試用例集合將針對原始的SCR表格實(shí)現(xiàn)分支覆蓋。此方法的測試準(zhǔn)則與結(jié)構(gòu)性測試準(zhǔn)則中分枝覆蓋準(zhǔn)則相似，這種覆蓋準(zhǔn)則與更嚴(yán)格的測試覆蓋準(zhǔn)則(如MC/DC)，對需求覆蓋的充分性還有待提高。

另外，Blackburn et al.提出了一種從SCR需求規(guī)格說明生成測試用例的方法，與眾不同之處是：此方法沒有采用模型檢查技術(shù)。目前已有基于此方法開發(fā)的商用軟件產(chǎn)品。

2.3 采用模型檢查方法的優(yōu)點(diǎn)

首先整個測試用例生成過程是規(guī)范化、形式化的。

其次，模型檢查器生成的用例提供的執(zhí)行路徑可以對基于需求的軟件實(shí)現(xiàn)進(jìn)行深度的遍歷。

模型檢查方法基于需求生成測試用例，以需求規(guī)格說明為依據(jù)，生成的測試用例中，針對相應(yīng)的系統(tǒng)輸入，給出了相應(yīng)的系統(tǒng)輸出，支持測試結(jié)果的自動化分析，可以提高測試效率。

2.4 形式化方法目前存在的不足

目前，基于模型檢查的用例生成方法主要存在以下3個方面的問題：

2.4.1 狀態(tài)爆炸問題

導(dǎo)致狀態(tài)爆炸的情況有以下2種：

(1) 模型中存在值域過大的整型類型的狀態(tài)變量，或者存在多個值域較大的整型類型的狀態(tài)量；

(2) 模型中存在數(shù)量龐大的狀態(tài)變量。

在進(jìn)行模型驗(yàn)證時，若發(fā)生狀態(tài)爆炸，模型檢查的時間將成幾何級的增長，由一般的秒級增長到小時級，另外，可能導(dǎo)致內(nèi)存溢出，根本無法完成模型檢查。

形式化模型能比較有效地描述輸入和輸出的約束關(guān)系，給定輸入，則會根據(jù)相應(yīng)的規(guī)定的規(guī)則和約束，由模型檢查器給出輸出結(jié)果。但對所有的輸入/輸出約束關(guān)系進(jìn)行描述將增大模型的狀態(tài)空間，可能引起狀態(tài)爆炸的問題。在功能結(jié)構(gòu)上如何有效地定義模型，是決定能否生成測試用例的關(guān)鍵：模型不能描述的太抽象，太抽象的模型雖然可以應(yīng)用于需求的形式化驗(yàn)證，但不能作為生成測試用例的模型；模型也不能描述的太細(xì)致，太細(xì)致的模型導(dǎo)致狀態(tài)爆炸或增加模型檢查的時間。目前解決狀態(tài)爆炸問題的方法之一是狀態(tài)抽象與簡化技術(shù)，如finite focus方法。

2.4.2 對需求中數(shù)值計算特性進(jìn)行描述的問題

目前的基于模型檢查的測試用例生成方法均未給出有效的、通用的描述需求中與數(shù)值計算相關(guān)的特性的方法。形式化語言能有效地定義輸入與輸出之間的邏輯型的約束規(guī)則，對于需求中的計算特性，由于形式化語言支持的基本數(shù)據(jù)只有有界整型、布爾型、枚舉型3種，無法描述需求中浮點(diǎn)型數(shù)據(jù)的值域，因此無法對其進(jìn)行有效的定義。

以形式化語言描述需求時，一般在建模時將需求中與計算特性相關(guān)的部分排除，主要對需求中的邏輯特性進(jìn)行建模。一般采用等價類劃分方法對計算的結(jié)果進(jìn)行等價類劃分，在需求模型中定義一個與之對應(yīng)的反映等價劃分的變量，這種方法無法精確地描述需求中的計算特性。模型檢查器生成的反例是構(gòu)造測試用例的依據(jù)，反例是一組輸入/輸出序列集合。在實(shí)際應(yīng)用中，浮點(diǎn)型數(shù)據(jù)類型在系統(tǒng)輸入數(shù)據(jù)中占較大的比例，且多個浮點(diǎn)類型數(shù)據(jù)之間的運(yùn)算結(jié)果作為某個功能的輸入條件，決定功能的輸出結(jié)果。如果不對這類影響功能輸出的數(shù)值計算特性進(jìn)行有效的定義，則生成的反例所包含的輸入/輸出序列中，輸入與輸出之間約束規(guī)則可能和實(shí)際需求中的輸入與輸出之間的約束規(guī)則不符，這樣的反例無法用于生成測試用例。

2.4.3 覆蓋充分性問題

目前常用的適合于模型檢查的結(jié)構(gòu)覆蓋準(zhǔn)則為分支覆蓋。但運(yùn)用結(jié)構(gòu)覆蓋準(zhǔn)則生成測試用例的有效性是比較低。狀態(tài)覆蓋，狀態(tài)遷移覆蓋，以及判定覆蓋同隨機(jī)生成的測試用例相比，發(fā)現(xiàn)錯誤的能力較差。通過模型檢查生成的反例通常比較短，由此轉(zhuǎn)換而成的測試用例的路徑也比較短，盡管覆蓋了所有要求覆蓋的結(jié)構(gòu)元素，但往往只是測試了形式化模型的小部分。如果對基于不同的覆蓋準(zhǔn)則生成的測試用例集進(jìn)行裁減，裁減后的測試用例集仍能滿足相應(yīng)的覆蓋準(zhǔn)則，但發(fā)現(xiàn)錯誤的能力卻大大降低。

2.4.4 由問題引發(fā)的思考

根據(jù)運(yùn)用模型檢查技術(shù)的經(jīng)驗(yàn)，針對狀態(tài)爆炸問題，可以在建模過程中，分析系統(tǒng)級的軟件執(zhí)行路徑，去掉不必要的狀態(tài)量，減小模型的規(guī)模，從而可以達(dá)到避免狀態(tài)爆炸的結(jié)果。同時，以有界整型數(shù)據(jù)模擬浮點(diǎn)型數(shù)據(jù)，借助形式化語言支持的四則運(yùn)算語法，定義與浮點(diǎn)計算相關(guān)的約束規(guī)則，從而在建立的形式化模型中有效地定義需求中的數(shù)值計算特性。

目前有一種更嚴(yán)格的覆蓋準(zhǔn)則，如MC/DC覆蓋準(zhǔn)則，提供了更好的發(fā)現(xiàn)錯誤的能力。

目前模型檢查生成測試用例的方法尚不能達(dá)到工程化的要求，做到測試用例自動生成的前提，還必須要根據(jù)軟件需求建立形式化模型，這一步的工作還不能實(shí)現(xiàn)完全的自動化，如果能夠?qū)⒁恍┚哂型ㄓ没墓δ苓M(jìn)行模塊提取，對其封裝以達(dá)到重用的效果，就能夠在建模的過程中提高效率。同時，還沒有一套完善的工具對整個形式化建模自動生成測試用例的方法進(jìn)行支持管理，所以這種方法的工程化程度還有待提高。

3 結(jié) 語

通過對目前國內(nèi)外測試用例自動生成方法的研究現(xiàn)狀進(jìn)行調(diào)研。本文按所其采用的方法和研究對象的不同，分別簡單地介紹了基于有限狀態(tài)集的測試，基于標(biāo)注的轉(zhuǎn)換系統(tǒng)的測試，針對面向模型的需求規(guī)格說明的測試以及針對面向?qū)ο筌浖臏y試。

對于目前運(yùn)用較多的模型檢查生成測試用例的方法，著重對此方法的原理和主要技術(shù)途徑進(jìn)行了詳細(xì)的分析和闡述，并列舉出其自身存在的優(yōu)勢與不足，同時給出了一些解決問題的方法探討。模型檢查在硬件和通訊協(xié)議的分析與驗(yàn)證中已經(jīng)取得了很大的成功，如何將這一技術(shù)應(yīng)用于軟件，是目前非?；钴S的研究領(lǐng)域。

參考文獻(xiàn)

[1]David Lee，Mihalis Yannakakis.Principles and Methods of Testing Finite State Machines-A Survey\\[J\\].In Proceedings of the IEEE，1996，84：1 090-1 123.

[2]Claude Jard，Thierry Jeeron.TGV：Theory，Principles and Algorithms\\[J\\].STTT，2005，7(4)：297-315.

[3]Robert M Hierons.Testing from a Z Specification\\[J\\].The Journal of Software Testing，Verification，and Reliability，1997，7(1)：19-33.

[4]Fletcher R，Sajeev A S M.A Framework for Testing Object Oriented Software Using Formal Specifications.In Reliable Software Technologies (Ada-Europe ′96)，Lecture Notes in Computer Science，Montreux，Switzerland，1996：159-170.

[5]Paul E Black.Modeling and Marshaling：Making Tests from Model Checker Counterexamples\\[C\\].In Proceedings of the 19th Digital Avionics Systems Conferences (DASC)，2000，1：1B3/1-1B3/6.

[6]Paul Ammann，Paul E Black.A Specification-based Coverage Metric to Evaluate Test Sets\\[J\\].In HASE，1999，IEEE Computer Society，1999：239-248.

[7]Paul Ammann，Paul E Black，William Majurski.Using Model Checking to Generate Tests from Specifications.In ICF-EM，1998.

[8]Kuhn D R.Fault Classes and Error Detection in Specification based Testing.ACM Transactions on Software Engineering Methodology，1999，8(4).

[9]Tai K C.Theory of Fault-based Predicate Testing for Computer Programs\\[J\\].IEEE Transactions on Software Engineering，1996，22(8)：552-562.

作者簡介 馬 亮 男，1982年出生，河北邯鄲人，碩士研究生。研究方向?yàn)樾问交椒ā?/p>

張 剛 男，1974年出生，山東淄博人，碩士生導(dǎo)師。研究方向?yàn)檐浖こ?、嵌入式系統(tǒng)、系統(tǒng)仿真。