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