在现在的测试过程中，形式化方法和测试方法的综合方法得到了广泛的关注，模型检测是其中较好的一种。近年来，模型检测被广泛的应用于各种实际问题中，其中包括硬件设计、协议分析、操作系统、容错和安全等等。
      这种形式化方法主要是采用了图论和有限状态机（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 来表示。可以使用模型检测器来找到一个方法达到这种状态，即通过将这个性质取反，例如不可能达到状态B，并要假设实际上也没有类似的输入序列，然后开始验证。在验证过程中，当模型检测发现了一个存在差异的公式时，可以产生一个反例，反例给出了一个验证序列，例如该序列说明可以使系统到达状态B，从而证明原性质实际上是可以被满足的；这个反例即构成了一个测试用例。
      通过对形式化模型中的每一个传输都重复这个过程，可使用模型检测器自动生成测试序列，可以得出覆盖模型的传输。
3 结论
   本文对结合模型检测来进行测试的方法进行了研究，该测试方法相对于传统的方法有很多优势：
   （1）从整体上对测试进行考虑，不仅包含了对系统所希望具有的功能进行测试，还包括了对系统不应具有的功能进行测试。
   （2）使用模型检测来代替部分的测试过程，而模型检测是自动进行的，这样大大降低了成本。
   （3） 通过系统规格模型Mspec 和系统实际执行模型Msyst的比较产生测试用例，这样可以有效控制测试的终止。通过这种方法，我们可以将模型检测应用于软件测试，进一步保证系统的正确性和可靠性。