1) 测试用例随机生成：采用随机游走的方式从系统的输入空间随机采样。但可能导致每次生成的测试用例集拥有不同的特征，目前常常将随机游走与用户操作版本相结合。
2) 专用的图搜索算法：包括结点覆盖、边覆盖算法。
3) 受限的模型检验：用来确认或者证伪一个系统的属性。对于特定的属性。如果属性不满足的时候。模型验证将输出一个反例。
4) 符号执行：它采用符号(如变量的名称)而不是实际的值来代表系统的输入，作为结果。执行过程中系统所有的变量及输出为符号或关于符号的表达式。
5) 演绎定理证明：与模型验证相似。用定理证明器代替了模型验证器。一般用来检查公式的可满足性。
4.7 联机、脱机测试用例生成
主要关注测试用例产生和执行的时机。在联机测试用例生成时，测试用例产生算法可以依据SUT的实际输出予以调整。这在SUT是非确定的时候是必要的。脱机测试用例生成意味着测试用例在生成结束后才能执行。脱机测试的一个优势是测试用例易于管理，因为测试用例变动较小。并且可以尝试采用最小化方法对测试用例规模进行缩减。 5
基于模型的测试的工具Spec Explorer
5.1 Spec Explorer
Spec Explorer[11]是微软发布的一款与Visual Studio紧密整合的基于模型测试的工具。用户可以通过Spec Explorer对一个软件系统的期望行为进行建模，并自动生成能够在Visual Studio的测试框架下运行的测试代码。模型可以用当前主流的程序设计语言C#开发，然后通过Cord语言脚本对模型进行配置和裁剪。
Spec Explorer[12]这个名字来源于该工具可以自动探索规格说明（即Specification，简称Spec）的所有潜在行为，并将其行为模型表示为状态机。一次探索的输出有可能非常巨大，所以Spec Explorer提供了Cord语言对输出进行裁剪，并选出测试中真正关心的场景。Spec Explorer能够高效的解决状态爆炸的问题。
5.2 连接测试用例和待测系统
Spec Explorer支持两种连接测试用例和待测系统的方式[13]：直接连接和适配
9
器连接。
直接连接是指将待测系统实现中的方法和事件直接声明成Cord配置中的Action（既可以依次声明也可以使用\all\提取所有公用方法），这样生成的测试代码会直接调用待测系统的方法，并期待待测系统的事件，如图5.1所示。这种连接只能被运用于测试托管代码实现的系统，并且要求待测系统提供的API足够进行测试。
图5.1 直接连接方式
测试适配器是则是位于测试用例和待测系统之间的一层。当创建测试适配器时，Cord配置文件中的Action并不是待测系统的方法和事件，而是适配器中的方法与事件；那么生成的测试代码也调用适配器中的方法，期待适配器发起的事件。适配器的作用是把这些方法调用转换为待测系统的方法调用，如图5.2所示。当待测系统是非托管代码实现，或者测试用例与待测系统需要远程通信，或者存在一个中间层用于抽象模型和测试（比如控制待测系统的用户界面）时，这种连接被广泛运用。适配器由于避免了对托管测试代码的依赖，从而极大的增加了spec Explorer的适用范围。
图5.2 测试适配器方式
模型开发者与适配器或者待测系统的实现者基于Action的接口规范打成一致，即可并行工作。接口实现只要在需要运行生成的测试代码时能够执行即可。
10
对于模型开发者来说，他们可以先把Action声明成abstract，即可在没有适配器或者待测系统实现的情况下进行建模。
5.3 静态模型和实例模型
Spec Explorer在使用过程中会让用户根据不同的情况选择不同的模型，主要分为2种类型的模型：静态模型和实例模型[14]。前面提到了两种连接测试用例与待测系统的方式：直接连接和适配器连接。如果你决定使用后者，那么适配器本身的设计决定了你选择静态模型还是实例模型。一个静态的适配器可以被用来控制一个基于实例的待测系统，反之亦然。考虑到测试适配器只是整个测试体系中的一个组件，所以这里进行选择的基本原理和设计任何一个面向对象的组件的基本原理是一致的。注意这里并不是一个是或者否的决定，静态和基于实例的Action可以共存于同一个适配器中。
Cord脚本中Action的声明被用于连接测试用例与待测系统或者适配器。总的来说，如果你的测试用例是调用待测系统或者适配器的静态方法，那么Action就应该是静态的；如果调用的是待测系统或者适配器的实例化方法，那么Action就是基于实例的。所以选择静态模型还是实例模型的决策权并不在建模者，而在于待测系统或者适配器的设计者。当然，两者可以是扮演不同角色的同一个人。
基于实例的Action意味着模型调用某一对象的方法，该对象不仅仅在模型探索阶段存在，在测试运行阶段也是存在的。所以该对象必须是之前某个步骤的输出，如果一个方法创建了一个没有返回的对象，那么显然这一对象不能在模型的后续步骤中被用到。
Spec Explorer允许把基于实例的Action与静态的模型方法进行对应（反过来亦可）。虽然一般来说不推荐这么做，因为基于实例的Action对应基于实例的模型方法，静态Action对应静态模型方法是很自然的设计，但是有时建模者不同意待测系统或适配器的设计，而希望用另一种模型设计。我们的目标是尽可能在满足需求的基础上让用户模型更为简单并更容易维护。 6
基于模型的测试的优缺点
与其他软件测试技术相比，基于模型的测试有以下优点[15]： 1. SUT的故障检测
软件测试的主要目的是发现SUT中的错误，事实证明，基于模型的测试可以很好的检测到故障数目。
2. 降低测试成本和时间
11
基于模型的测试在编写和维护模型上花费的时间和精力要低于手工测试中设计和维护一个测试套件的投入成本。
3. 提高测试质量
手工测试的质量依赖于富有创造力的测试工程师，每个测试用例产生的原因是不会记录的，并且这些测试用例不容易涉及到初始的系统需求。基于模型的测重复化。通过考虑模型的覆盖就可以测量测试套件的―质量‖。同时，基于模型的测试相比手动测试可以用来生成更多的测试。通过改变模型的测试选择标准或者告诉工具来生成更多的测试，我们可以很容易地获得非常大的测试套件，这可以帮助发现更多的错误。
4. 需求缺陷检测
一个有时意想不到的好处是对于非正式的需求，基于模型的测试可以通过编写模型来暴露问题的所在，而这些需求通常是记录在一个大型的、可能包含遗漏、矛盾的、不清楚的自然语言文档中。基于模型的测试的第一步就是通过构建一个抽象模型SUT来澄清这个预期的行为，这个模型要求具有精确的语义，以便它可以分析一个机器。所以建模阶段通常要求公开许多问题。
5. 可追溯性
可追溯性是能够涉及到模型中每个测试用例，测试选择标准，甚至到非正式的系统需求。可追溯性有助于解释测试用例的生成原因，也可以在模型发展时优化测试执行。例如，当我们使用UML状态机作为建模表示法，测试生成算法会记录模型的哪些转换被用于每个测试用例。
6. 需求的演变
手工测试中，如果测试设计和系统的需求变化，大量的工作经常需要花费在更新测试套件上来反映新的需求。基于模型的测试可以通过更新模型来重新测试，因为模型通常远小于测试套件，这样就可以花费更少的时间来应对不断变化的需求。并且使用工具分析新旧需求的差异，还可以报告哪些测试不再相关，哪些测试涉及修改后的需求，哪些测试是新加的。所以，一个需求改变后，相应变化的模型可以将测试分为：删除、不变、改变、新增四组。当测试时间有限的情况下，只执行后两组是非常有用的。
正是由于基于模型的测试具有诸多优点，可以解决许多其他测试技术不能解决的问题，所以在WEB应用测试、通信协议测试等复杂系统中具有广泛的应用。
不过，基于模型测试也不是万能的，也存在一些局限性： 1．过时的需求
作为一个软件工程的发展，有时非正式的需求变得过时了。如果一些基于模型的测试人员从过时的需求开始工作，他们将建立错误的模型，这样就会在SUT
12
找到大量的―错误‖。
2．不适当使用基于模型的测试
基于模型的测试并不是一颗可以迅速发现程序每个漏洞的子弹，也不会比标准的自动化测试流程更有效或更经济。它的作用是在输入准确的前提下为复杂的项目(比如实时或嵌入式程序设计)实现有实际价值的、非重复性模拟测试。
3．分析失败的测试时间
当一个生成的测试失败，我们必须决定是否由于SUT、适配器代码或错误的模型引起。基于模型的测试生成测试序列相比手工设计的测试序列可能会更复杂，这就使得发现导致失败的测试更加困难和耗时。
4．无用的指标
当测试设计，大多数经理使用手动测试用例的数量作为衡量设计测试进展顺利。但基于模型的测试容易产生大量的测试，所以测试数量指标是没有用的。有必要引入其他的测量测试方法，如SUT代码覆盖率，需求覆盖率，和模型覆盖率。
参考文献
[1]毛澄映, 卢炎生. 构件软件测试技术研究进展[J]. 计算机研究与发展, 2006, 43(8):1375-1382.
[2] Schieferdecker I. Model-Based Testing [J]. IEEE Software, 2012, 29(1):14-18. [3] Bouquet F, Dadeau F, Legeard B, et al. JML-Testing-Tools: A Symbolic Animator for JML Specifications Using CLP.[M]// Tools and Algorithms for the Construction and Analysis of Systems. Springer Berlin Heidelberg, 2005:551-556.
[4] Harel D. Statecharts: a visual formalism for complex systems[J]. Science of Computer Programming, 1987, 8(3):231-274.
[5] Avritzer A, Larson B. Load Testing Software Using Deterministic State Testing.[M]. ACM, 1993.
[6] Hoorn A V, Rohr M, Hasselbring W. Generating probabilistic and intensity-varying workload for web-based software systems[C]// Performance Evaluation – Metrics, Models and Benchmarks: Proceedings of the SPEC International Performance Evaluation Workshop (SIPEW ’08), volume 5119 of Lecture Notes in Computer Science (LNCS. 2008:124--143.
[7] Poore J H. Introduction to the special issue on: model-based statistical testing of software intensive systems[J]. Information & Software Technology, 2000, 42(12):797-799.
13
[8] Maurer P M. The Design and Implementation of a Grammar-based Data Generator.[J]. Software Practice & Experience, 1992, 22(3):223-244.
[9] Pretschner A, Philipps J. 10 Methodological Issues in Model-Based Testing[J]. Lecture Notes in Computer Science, 2005, 3472:11-18.
[10] Lamsweerde A V. Formal specification: a roadmap.[J]. Future of Software Engineering A Finkelstein Acm, 2000:147-159. [11]xianglims.
百
度
百
科
Spec
Explorer.
[EB/OL].[2016-01-18].
http://baike.http://www.wodefanwen.com//link?url=wGJJPEPVVYUNI5dn69s9uJKp1p4iw7FyNtj0TlMZ8eaRDxdt-uWt_tnTIbzJ_IJoS-sKhaMiBqlcgg1BUfa84_.
[12]朱永光. 用Spec Explorer进行基于模型的测试. [EB/OL].[2016-01-18]. http://www.infoq.com/cn/news/2009/11/spec-explorer-2010
[13]Xiang Li. Spec Explorer连接测试用例与待测系统. [EB/OL].[2016-01-18]. http://blogs.msdn.com/b/sechina/archive/2009/12/22/9940058.aspx.
[14]Xiang Li. Spec Explorer静态模型和实例模型. [EB/OL].[2016-01-18]. http://blogs.msdn.com/b/sechina/archive/2009/12/22/9940059.aspx
[15] 吴艳, 张惠. 基于模型的软件测试方法研究[J]. 计算机系统应用, 2008, 17(8):87-89.
14