在現在的測試過程中，形式化方法和測試方法的綜合方法得到了廣泛的關注，模型檢測是其中較好的一種。近年來，模型檢測被廣泛的應用于各種實際問題中，其中包括硬件設計、協議分析、操作系統、容錯和安全等等。
      這種形式化方法主要是采用了圖論和有限狀態機（Finite State Machine FSM）原理來驗證被測試系統（system under test SUT）的性質，并通過以狀態為基礎模型來描述系統的行為。通過一個模型檢測器遍歷模型中所有可達的狀態，并檢驗其是否符合系統
     所期望的性質。系統的性質由時態邏輯公式（temporallogic formulate TLF）進行描述，并要求這些性質滿足所有可能的路徑。若有一個性質不能滿足，則模型檢測器以狀態序列的形式產生一個反例。
     目前已經提出了一些方法，本文的方法有所不同，從整體上對測試進行考慮，不僅包含了對系統所希望具有的功能進行測試，還包括了對系統不應具有的功能進行測試。
1 模型檢測中的相關定義
      模型檢測通過搜索系統的狀態空間來確認系統是否具有所希望的性質（或不具有所不希望的性質）。其基本思想是使用狀態遷移系統（S）表示系統的行為，用模態/ 時序邏輯公式（F）描述系統的性質。
     這樣“系統是否具有所期望的性質”轉化為數學問題“狀態遷移系統S 是否是公式F 的一個模型”，對有限狀態系統，這個問題是可判定的，即可以用計算機程序在有限的時間內自動確定。在初始階段，建立的模型要符合系統所期望完成的功能，
模型Mspec 是符合用戶對系統功能要求的規格模型，如果要進行驗證，則需要另一個模型來描述所觀察到的系統行為，即系統模型Msyst。
     本文中增加了一個對系統不應具有的性質進行描述的模型M’spec，通過這個模型可以對系統不應具有的功能進行測試。本文中我們用有限狀態機（Finite State Machine FSM）來對Mspec進行描述。
     定義1：一個FSM可以通過一個三元組（S， R， S0）來描述，其中S 是一個有限狀態集，S×S→R 表示傳輸關系，S0∈S 表示初始狀態。對于任意（s1，s2）∈R，表示FSM中的一條邊。
在模型檢測中，測試用例用線性時態邏輯（lineartemporal logic LTL）對公式φ 進行描述。公式φ 的描述如下。
定義2：若P 是一個原子命題則P 是一個公式。
定義3：類似于組合φ，φ1∧φ2，φ1∨φ2，Xφ1，Fφ1，φ1Uφ2，φ1Rφ2 的形式都是公式。
定義4：若在眾多狀態的一個無限序列上的這些時間操作有如下含義，其被稱為路徑。X(neXt) 規定路徑上的下一個狀態的性質F(Future) 判定路徑上的一些狀態是否具有某種性質G(Global) 定義路徑上的每一個狀態的性質U (Until) 若路徑上的一個狀態處于第二個性質下，并且路徑上的每一個前趨狀態處于第一個性質下，則保持。
       R(Release)是對U 的邏輯取反。要求路徑上保持第二種性質直到出現第一個保持第一個性質的狀態。但是第一個性質不需要一直保持。在本文中用Kripke 結構來表示系統模型Msyst。定義5：AP 表示一組原子命題，Kripke 結構M是
       一個四元組（S， S0， R， L），其中S 是一個有限狀態集，S0∈S 表示初始狀態，S×S→R 表示傳輸關系，L 是映射L：S→2AP ，表示原子命題在該狀態為真。
2 基于模型檢測的測試方法
     Mspec 模型是在SUT 的構建初期以其規格為基礎進行建模得到的，Msyst 模型是根據SUT 的實際運行過程得出的，M’spec 模型是對SUT 不應具有的性質進行描述的模型。通過引入M’spec 模型，我們可以對系統不應具有的功能進行描述，并以此對系統進行更為全面的測試。
     其中使用了控制流（實線）表示活動，使用了數據流（虛線）來表示輸入和輸出的活動。其中，數據流的主要部分是SUT、規格、Mspec、M’spec、Msyst 模型。選擇和應用測試用例可依據以下方法進行：FSM中的狀態轉移表示測試用例，在測試過程中，要求FSM中所有的邊都可被測試用例覆蓋。
     對于被選定的測試用例，需要被表示成LTL 公式的形式，并被看成是模型檢測中的性質。只要在模型檢測過程中出現了不一致，表明檢測出了錯誤。這個錯誤可能是由于SUT、Mspec、Msyst 模型或規格本身的錯誤引起的。對錯誤的查找可以從SUT 開始。
概括的說，這個方法是通過Mspec 模型和Msyst 模型的比較來發現模型之間的差異。這些差異中的任何一個都是對錯誤進行正確定位的關鍵因素，定位是通過這樣的一個過程完成的：首先檢查差異是否是因為SUT 中的錯誤引起的，如果不是，接下來檢查Msyst 模型，若引起差異的原因是在于Msyst 模型，則用戶對于系統的錯誤理解需要糾正一下了，其它例如規格和Mspec 中的錯誤也通過類似的方法檢查。每當有一個差異被確認后，便可以通過一個確定的方法對錯誤進行定位。這個過程在有限的測試用例集中的測試用例用盡時終止。
   通過這個方法，我們可以通過規格來產生測試用例，并將其表示成為Msyst 模型檢測中的性質。舉例來說，我們希望對系統中的狀態A 和B 之間的傳輸進行測試，這個傳輸是在C 環境下進行的，我們可以把測試用例對這個傳輸進行測試的條件進行公式化的描述：序列的輸入必須可以使模型到達狀態A，在狀態A，C 必須為真，并且下一個狀態必須是B。這些性質可以用LTL 來表示？梢允褂媚Ｐ蜋z測器來找到一個方法達到這種狀態，即通過將這個性質取反，例如不可能達到狀態B，并要假設實際上也沒有類似的輸入序列，然后開始驗證。在驗證過程中，當模型檢測發現了一個存在差異的公式時，可以產生一個反例，反例給出了一個驗證序列，例如該序列說明可以使系統到達狀態B，從而證明原性質實際上是可以被滿足的；這個反例即構成了一個測試用例。
      通過對形式化模型中的每一個傳輸都重復這個過程，可使用模型檢測器自動生成測試序列，可以得出覆蓋模型的傳輸。
3 結論
   本文對結合模型檢測來進行測試的方法進行了研究，該測試方法相對于傳統的方法有很多優勢：
   （1）從整體上對測試進行考慮，不僅包含了對系統所希望具有的功能進行測試，還包括了對系統不應具有的功能進行測試。
   （2）使用模型檢測來代替部分的測試過程，而模型檢測是自動進行的，這樣大大降低了成本。
   （3） 通過系統規格模型Mspec 和系統實際執行模型Msyst的比較產生測試用例，這樣可以有效控制測試的終止。通過這種方法，我們可以將模型檢測應用于軟件測試，進一步保證系統的正確性和可靠性。