測試用例自動生成方法的現狀及研究

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

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

中圖分類號：TP311 文獻標識碼：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

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

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

1 特定領域生成測試用例方法現狀

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

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

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

(1) 基于有限狀態機的測試；

(2) 基于標注的轉換系統(LTS)的測試；

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

(4) 針對面向對象軟件的測試；

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

以上的一些方法已有與之對應的原型工具，有些已經投入到實驗中，另外，當前已有一些商業化的測試輔助工具，支持自動生成測試用例的功能。在以上5種測試用例自動生成方法中，除模型檢查方法之外，其他4種方法主要適用于特定的應用領域。基于模型檢查的測試用例生成方法是目前被廣泛研究的一種確認測試用例生成方法，已有一些階段性的研究成果。

1.1 基于有限狀態機的測試

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

基于有限狀態機的測試的應用的領域較小，但其思想常體現在需求描述和形式化建模中，針對需求的描述方法中就有狀態圖描述法。實際上，根據需求建立的形式化模型可以看作一個有限狀態機。

1.2 基于標注的轉換系統的測試

標注的轉換系統(LTS)主要用于描述以特定的需求規格說明語言定義的系統行為，例如，程序代數(如LOTOS)是一種語義模型為LTS的運用廣泛的語言。一個標注的轉換系統(LTS模型)包括狀態和狀態之間的標注的狀態遷移，以狀態模擬系統的狀態，以狀態遷移對系統與系統周圍的環境發生的交互進行模擬。LTS模型通常以圖或樹的形式描述系統行為以及改變系統狀態的事件，其中邊被標注為事件，代表狀態遷移，而節點代表狀態。針對LTS系統，已開發出許多測試工具，這些測試工具都是基于ioco測試理論，其中一個比較著名的工具是TorX^[2]。

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

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

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

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

1.4 針對面向對象軟件的測試

目前大多數的軟件系統采用傳統的結構化方法進行設計，即面向結構的軟件，例如目前的航天型號軟件，基本都是通過結構化方法進行設計開發，很少采用面向對象方法進行設計和開發。目前在軟件開發領域，面向對象方法已被廣泛接受與運用，出現了大量的運用面向對象方法開發的軟件。測試面向對象的程序和測試結構化方法設計出的程序有很大的差異，因為，在一種環境下某一個被充分測試的面向對象組建在任何其他的環境中不一定意味著其已經被充分的測試到。因此，出現了許多特定的針對面向對象軟件進行測試的研究。

目前此領域的研究進展如下：OZTest是針對面向對象程序的半自動的生成測試用例的框架，以Object-Z作為形式化的需求規格說明語言。Object-Z是一種基于模型的面向對象的語言。

由于目前的航天型號軟件基本上采用結構化方法進行設計開發，因此針對面向對象軟件的測試目前不適合應用于航天型號軟件測試。隨著技術的發展，面向對象方法可能會被航天型號軟件采用，則可以采用此方法對型號軟件進行測試^[4]。

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

2 運用模型檢查生成測試用例方法

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

2.1 運用模型檢查生成測試用例的原理

因具有在驗證系統特性時可產生反例的特點，模型檢查技術被人們所關注，作為生成測試用例的引擎。

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

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

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

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

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

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

2.2 主要技術途徑

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

2.2.1 基于運算符變異的技術

基于運算符變異的思想的理論基礎是耦合效應猜想，即在測試中，存在這樣一種現象：能檢測出簡單錯誤的測試用例有可能同時檢測出復雜的錯誤。其方法是運用變異運算符對系統的描述進行小的改變，例如，對變量的改變。

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

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

2.2.2 通過構造陷阱特性結合

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

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

2.3 采用模型檢查方法的優點

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

其次，模型檢查器生成的用例提供的執行路徑可以對基于需求的軟件實現進行深度的遍歷。

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

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

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

2.4.1 狀態爆炸問題

導致狀態爆炸的情況有以下2種：

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

(2) 模型中存在數量龐大的狀態變量。

在進行模型驗證時，若發生狀態爆炸，模型檢查的時間將成幾何級的增長，由一般的秒級增長到小時級，另外，可能導致內存溢出，根本無法完成模型檢查。

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

2.4.2 對需求中數值計算特性進行描述的問題

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

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

2.4.3 覆蓋充分性問題

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

2.4.4 由問題引發的思考

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

目前有一種更嚴格的覆蓋準則，如MC/DC覆蓋準則，提供了更好的發現錯誤的能力。

目前模型檢查生成測試用例的方法尚不能達到工程化的要求，做到測試用例自動生成的前提，還必須要根據軟件需求建立形式化模型，這一步的工作還不能實現完全的自動化，如果能夠將一些具有通用化的功能進行模塊提取，對其封裝以達到重用的效果，就能夠在建模的過程中提高效率。同時，還沒有一套完善的工具對整個形式化建模自動生成測試用例的方法進行支持管理，所以這種方法的工程化程度還有待提高。

3 結 語

通過對目前國內外測試用例自動生成方法的研究現狀進行調研。本文按所其采用的方法和研究對象的不同，分別簡單地介紹了基于有限狀態集的測試，基于標注的轉換系統的測試，針對面向模型的需求規格說明的測試以及針對面向對象軟件的測試。

對于目前運用較多的模型檢查生成測試用例的方法，著重對此方法的原理和主要技術途徑進行了詳細的分析和闡述，并列舉出其自身存在的優勢與不足，同時給出了一些解決問題的方法探討。模型檢查在硬件和通訊協議的分析與驗證中已經取得了很大的成功，如何將這一技術應用于軟件，是目前非常活躍的研究領域。

參考文獻

[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年出生，河北邯鄲人，碩士研究生。研究方向為形式化方法。

張 剛 男，1974年出生，山東淄博人，碩士生導師。研究方向為軟件工程、嵌入式系統、系統仿真。