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