基于模型的测试报告

基于模型的测试综述2016年1月目录TOC\o"1-3"\h\u13447摘要 I160911引言 2233352基于模型的测试、模型以及建模标准 216952.1基于模型的测试 2114112.2基于模型的测试的模型 313582.3建模标准 441643基于模型的测试的基本过程及支持工具 543843.1基于模型的测试的基本过程 5178613.2支持工具 6278634分类 7103874.1模型主体 788884.2模型冗余程度 7111814.3模型特征 7277294.4模型表示法 748154.5测试用例选择标准 8136394.6测试用例生成技术 8241844.7联机、脱机测试用例生成 9311755基于模型的测试的工具SpecExplorer 9187275.1SpecExplorer 913595.2连接测试用例和待测系统 9264815.3静态模型和实例模型 11319756基于模型的测试的优缺点 1118915参考文献 13引言在软件开发的生命周期中，测试是一个非常重要的阶段。软件测试[1]通过为特定测试目的而设计的测试用例的执行情况，与预期的软件行为进行一致性对比，从而判定软件错误所在，以此确保软件的可靠性和正确性。由于软件产品的固有的复杂性质，软件测试的难度也就不言而喻。传统的测试方法被认为是繁琐的、强工作量且容易出错。应运而生的基于模型的测试开始受到日渐广泛的关注。基于模型的测试（Model-BasedTesting）[2]是一种系统化的测试方法，可被应用于软件生命周期早期阶段的产品的测试，并且它使完全自动化测试成为可能，其特点是：在产生测试例和进行测试结果评价时，都是根据被测试应用程序的模型及其派生模型（一般称作测试模型）进行的。基于模型的测试深受工业界的青睐，原因如下：一是工业界通常需要验证软件产品的系统行为。在产品设计的早期，基于模型的测试的使用有利于帮助找出不清晰的、易存在二义性的软件系统规格说明（“即编码前的分析设计模型/文档”）。二是基于模型的测试方法使得大量不重复的、有意义的测试用例产生变得可能。三是使用基于模型的测试一旦系统规格说明发生改变，只需要对测试模型进行修改就可以轻松地达到更新测试用例的目的。本文组织如下，首先介绍了基于模型的测试及其特点，分析了主要的测试模型及如何选择合适的测试模型，重点是有限状态机模型、UML模型和马尔可夫链模型，并且提出了建模的标准；接着介绍基于模型的测试的基本过程以及支持工具，再通过七个维度对基于模型的测试方法进行描述，并对每一个维度探讨了可能取值，然后与其他软件测试技术相比，分析基于模型的测试的优缺点，最后列举了一些基于模型的测试的应用案例。基于模型的测试、模型以及建模标准2.1基于模型的测试首先应该要明确软件模型的概念，是指用抽象化的方式对软件行为和软件结构进行阐述，软件行为可以通过一系列的输入输出逻辑和数据流分析来表示，软件结构则是通过部署图、流程图等图形方式直观表述，基于模型的测试就是通过上述两种抽象化方式产生测试用例。相比于针对程序代码本身的测试，而基于模型的测试方法不仅可以有效地提高测试效率，提高测试例生成的自动化程度，进行测试失效辨识，也有利于评价测试结果。基于模型的测试是对被测系统的模型化，然后根据模型特性，完全或者部分地自动生成测试用例的一种软件测试技术。基于模型的测试是一个轻量级的，形式化的验证软件系统的方法。首先，基于模型的测试对待测软件系统（通常被称为SystemUnderTest，简称SUT）进行形式化的建模，设计出机器可读的模型；其次，和其他形式化方法比，基于模型的测试并不致力于让待测软件系统与规格说明在所有可能情况下都保持一致，而是系统化的从模型生成一组测试用例，使用这组测试用例测试待测软件系统，得到充分的证据说明待测系统的行为与模型期望是一致的。2.2基于模型的测试的模型理想的模型需要容易被测试人员理解，能够把大的复杂的问题描述成小的简单的系统，最好还是以一种测试用例生成工具方便识别的形式。想要同时满足以上所有的特性是很困难的，但是可以把几种不同的模型整合成一个，扬长避短地得到理想模型。在基于模型的测试中使用过的模型可能有几十甚至上百种，我们不可能也没有必要去逐一了解，MarkUtting和BrunoLegeard把它们大致分为以下几种[3]：表2.1MBT模型分类类型示例基于Pre/PostB、OCL、JML、Spec#、Z基于转换FSM、状态图、UML状态机统计式马尔可夫链基于历史消息队列图、UML顺序图函数式HOL系统操作式Petri网数据流式Lustre、块状图基于模型的测试中使用的典型模型有:有限状态机（FSM，FiniteStateMachine）、UML模型和马尔可夫链等模型。有限状态机该类模型是用状态转移图来表示，并通过状态的覆盖来生成测试用例。这种模型可以将测试用的数据结合图的遍历算法自动生成输入的序列进行相应测试。该种测试模型可以充分结合形式语言与自动机理论来进行分析和设计，适用范围主要是反应式的软件，但由于模型构造的工作规模比较大，自动构造就成为了这一模型的一个关键点。UML模型又称为统一建模语言，是软件工程中面向对象设计与分析中常用到的规范化建模语言。该模型主要是利用状态图进行行为建模，状态图可以看作是有限状态机的扩展，强调了对复杂实时系统进行建模，提供了层次状态机的框架，即一个单独状态可以扩展为更低级别的状态机，并提供了并发机制的描述[4]，因此UML使用状态图作对单个类的行为建模。马尔可夫链是一种以统计理论为基础的统计模型，可以描述软件的使用在软件统计测试中得到了广泛应用。马尔可夫链实际上是一种迁移具有概率特征的有限状态机，不仅可以根据状态间迁移概率自动产生测试例，还可以分析测试结果对软件性能指标和可靠性指标等进行度量[5,6]。另外，马尔可夫链模型适用于对多种软件进行统计测试，并可以通过仿真得到状态和迁移覆盖的平均期望时间，有利于在开发早期对大规模软件系统进行测试时间和费用的规划。马尔可夫链是统计测试的基本模型，在净室软件工程中得到了深入研究，在微软、Raytheon及美国联邦航空署(FAA）都得到了成功应用[7]。马尔可夫链可以用随机迁移矩阵或者带迁移概率的状态迁移图表示。基于马尔可夫链的测试充分性准则一般要求测试过程中对马尔可夫链迁移的覆盖与实际使用相同[6]。文法模型可以描述程序的语法。由于不同的文法等价于不同的状态机因此也可以视为状态机模型的变体。有关基于文法的测试可见文[8]，这方面研究工作相对较少。2.3建模标准随着系统的增长，建模是捕获和再利用有关系统知识的一个非常经济的手段。对于一个测试团队来说，这些信息是非常宝贵的：一个测试工程师了解被测系统的行为需要占据的工作量，一旦这个信息被理解，该如何保存给下一个工程师、下一个版本或者更改要求呢？如果你处于测试的设计阶段，那么你是幸运的。但是更常见的是，这些信息被埋藏在一个测试脚本中，一旦改变或者丢失就只能等待重新发现。测试团队通过给系统构建一个给予指定输入得到所需行为的模型，可以获得有重用的最大优势就是这些工作都不会丢失。一旦这个测试周期停止，下一周期就可以迅速开始。如果该产品具有新的功能，它们可以逐步加入到模型中；如果产品的质量需要提高，那么模型需要改善和扩大测试；如果有新的人员加入到测试团队中，他们可以通过回顾模型迅速投入进来。一旦你决定想要为被测系统建模，下一步建模的时候要思考这个系统管理的数据、执行的操作和与它通信的子系统。下面给出几条原则：1．抽象原则，通常不把输入、输出纳入到模型中。2．模型与被测系统不必完全一致。基于模型的测试的基本过程及支持工具3.1基于模型的测试的基本过程基于模型的测试的基本过程共有6个步骤，如图2.1所示，其步骤如下：分析被测系统首先分析被测软件的系统特性，主要分析的是开发方式，主要有所采用的开发技术(面向对象、面向过程)，开发语言，开发系统环境等。然后根据分析结果，结合各个模型的特性选择合适的模型作为测试用例生成的模型。建立抽象模型根据所选择的模型对被测软件进行建模，可以进一步分析该模型是否适合软件。模型选择和建立模型可能是个反复的过程，只有在充分了解该软件系统的特点和各个模型的特点才可能为软件系统建立最恰当的模型。这个模型是一个抽象模型，因为它应该比待测软件系统（通常被称为SystemUnderTest，简称SUT）本身更小，更简单，它只关注关键环节。建立完成后，需要检查该模型与所期望的行为是否一致。生成抽象测试从模型生成抽象测试，必须选择一些测试选择标准，因为通常有无限多的可能的测试。比如使用有限状态机FSM模型时，根据一定的覆盖准则遍历状态间的迁移所获得的转换路径就是测试路径，而且在使用FSM模型时选择不同的测试覆盖准则所产生的测试用例是不同的。具体化抽象测试基于模型的测试的第四步是把高层的抽象测试转化为可执行的具体测试。主要有两种方法：(1)使用模板和映射抽象测试的变换工具；(2)通过一些环绕在SUT和代码实现间的适配器。执行具体测试基于模型的测试的第五步是在被测系统上执行具体的测试用例，不管是在在线的还是离线的基于模型的测试，都可以使用测试执行工具和方法。分析测试结果得到测试结果后，必须确定产生该故障的原因并采取纠正措施，因为有可能是建模时的缺陷模型导致的测试用例本身故障。然后根据测试结果和分析结果，评估被测软件的质量，并且指出出错的地方和提出改进的意见和建议。图2.1基于模型的测试过程3.2支持工具基于模型的软件测试必须有相关工具支持。当前支持基于模型的软件测试工具中比较具有代表性的有：支持状态机模型的工具。包括，SoftwareEngineeringTechnology的测试工具toolSET_Certify运行于RISC6OOO和SUN平台；现在此工具属于G-Lab，并已经提供了对统计测试的支持；IBM的GOTCHA,可以根据用户事先确定的测试充分性准则进行基于软件状态模型的测试例生成；IBM的TCBean是一个提供测试脚本管理功能的基于状态机的测试引擎。支持马尔可夫链模型的工具。包括，CleanroomSoftwareEngineering的CleanTest，支持统计测试，是商用的使用模型及统计测试例生成工具；IBM的CleanroomCertificationAssistant，可以自动化统计验证过程，通过使用概率分布产生测试例，并对测试结果进行分析。对UML模型提供测试支持的工具。包括，SilverMark公司针对IBM公司的VisualAge开发的支持测试用例生成和回归测试的TestMetor和UMLdesignerConnection。对统计测试结果进行分析的工具。包括AT&ST的软件可靠性工程工具箱和美国海军水面战中心开发的SMERFS，均提供多种时间域和区间域模型进行可靠性估计;美国空军喷气动力实验室开发的CASRE，支持可靠性估计和预测。分类本文通过七个维度对基于模型的测试方法进行描述。并对每一个维度探讨了可能取值。4.1模型主体模型主体包括SUT模型和SUT所处环境模型。目前基于模型的软件测试中往往两者都同时考虑。SUT模型的作用包括：(1)作为SUT的oracle(因为SUT包含了预期行为)；(2)利用结构信息产生测试用例。SUT所处环境模型用于限制SUT模型的可能输出。4.2模型冗余程度基于模型的测试可以被应用到不同的场景。大致说来，主要区别在用于测试和用于实现的模型间的冗余程度。文献[9]中描述了两个可能场景。第一个场景中模型被用来同时产生测试用例和系统实现。该场景中用于产生代码的模型必须描述详细，但对测试用例生成来说确需要抽象级别更高的模型。第二个场景是：模型仅用于产生测试用例。该模型根据规约文档生成，而SUT则是手工实现。我们可以使用该模型作为系统的规约补充，但其相当复杂。往往需要补充文档辅助才能使用。4.3模型特征模型特征与非确定性、时序问题、模型的连续性或事件离散性有关。非确定性在SUT和模型中均会发生。时序问题一般与实时系统相关。而就动态性而言。模型可能是离散的、连续的或两者综合。基于模型的软件测试过去往往关注离散模型，但连续或者混合模型目前在嵌入式系统中得到广泛使用和研究。不同的模型特征将影响对模型表示法的选择、测试用例的生成和执行。4.4模型表示法目前存在大量模型范式对SUT进行建模，根据[10]获得如下的分类：基于状态的表示法：针对变量集和修改变量的操作对系统进行建模，变量集代表系统内部状态的一个快照，操作通过前置条件和后置条件定义。典型代表为Z、B、VDM和JML。基于Transition的表示法：描述不同系统状态间的transition。采用类似FSM的形式进行表示。结点代表系统的状态，边代表系统的操作或行为。目前常通过添加数据变量、采用分层的机器和机器之间的并行来加强表示能力。典型代表为Statecharts．hbeledtransitionsystem和I／Oautomata。基于历史的表示法：通过描述随着时间的推移，行为允许的轨迹对系统进行建模。可以使用不同的类型的时间记号(离散或连续，线性或分支，点或区间等)，导致了不同类型的时序逻辑。函数表示法：将系统描述为数学函数集。有可能是一阶的也有可能是多阶的。但该类表示法较为抽象和难于使用。所以在基于模型的测试中使用并不多。操作表示法：认为系统是可执行进程集，进程间并行执行。该表示法适合描述分布式系统或通讯协议。典型代表是进程代数或者Petrinet。随机表示法：通过基于事件或者输入值的概率模型来描述系统，更倾向于为环境建模。例如使用Markovchain为期望的用户操作版本建模．据此产生的测试用例集可以体现用户的实际使用场景。4.5测试用例选择标准测试用例选择标准可以辅助测试用例的生成。目前并不存在一个最优标准。普遍使用的标准包括：结构化模型覆盖标准：标准充分利用了模型结构信息，例如在基于transition的模型中。采用与图相关的覆盖标准来生成测试用例。数据覆盖标准：标准主要关注如何从大规模数据空间里面选择典型取值。常见的方式是等价类划分和边界值分析。基于需求的覆盖标准：当模型的元素与SUT的非形式化需求相关时，需要基于需求的覆盖标准。例如：需求数量可能与UML状态图的transition有关。Ad—hoc测试用例规约：除了模型，测试工程师可以依据经验，用形式化的表示方法编写必须覆盖的测试用例规约。指定对应的测试用例。随机标准：大部分用于环境模型。因为是环境决定了SUT的使用方式。行为概率直接用模型表示。产生的测试用例反应了用户的实际操作情况。基于缺陷的标准：适用于SUT模型。最常见的基于缺陷的覆盖标准是变异覆盖。包括对模型进行变异、产生测试用例用于区分变异模型和原有模型。4.6测试用例生成技术目前在给定SUT模型和测试用例规约下。主要包括如下技术：测试用例随机生成：采用随机游走的方式从系统的输入空间随机采样。但可能导致每次生成的测试用例集拥有不同的特征，目前常常将随机游走与用户操作版本相结合。专用的图搜索算法：包括结点覆盖、边覆盖算法。受限的模型检验：用来确认或者证伪一个系统的属性。对于特定的属性。如果属性不满足的时候。模型验证将输出一个反例。符号执行：它采用符号(如变量的名称)而不是实际的值来代表系统的输入，作为结果。执行过程中系统所有的变量及输出为符号或关于符号的表达式。演绎定理证明：与模型验证相似。用定理证明器代替了模型验证器。一般用来检查公式的可满足性。4.7联机、脱机测试用例生成主要关注测试用例产生和执行的时机。在联机测试用例生成时，测试用例产生算法可以依据SUT的实际输出予以调整。这在SUT是非确定的时候是必要的。脱机测试用例生成意味着测试用例在生成结束后才能执行。脱机测试的一个优势是测试用例易于管理，因为测试用例变动较小。并且可以尝试采用最小化方法对测试用例规模进行缩减。基于模型的测试的工具SpecExplorer5.1SpecExplorerSpecExplorer[11]是微软发布的一款与VisualStudio紧密整合的基于模型测试的工具。用户可以通过SpecExplorer对一个软件系统的期望行为进行建模，并自动生成能够在VisualStudio的测试框架下运行的测试代码。模型可以用当前主流的程序设计语言C#开发，然后通过Cord语言脚本对模型进行配置和裁剪。SpecExplorer[12]这个名字来源于该工具可以自动探索规格说明（即Specification，简称Spec）的所有潜在行为，并将其行为模型表示为状态机。一次探索的输出有可能非常巨大，所以SpecExplorer提供了Cord语言对输出进行裁剪，并选出测试中真正关心的场景。SpecExplorer能够高效的解决状态爆炸的问题。5.2连接测试用例和待测系统SpecExplorer支持两种连接测试用例和待测系统的方式[13]：直接连接和适配器连接。直接连接是指将待测系统实现中的方法和事件直接声明成Cord配置中的Action（既可以依次声明也可以使用"actionall"提取所有公用方法），这样生成的测试代码会直接调用待测系统的方法，并期待待测系统的事件，如图5.1所示。这种连接只能被运用于测试托管代码实现的系统，并且要求待测系统提供的API足够进行测试。图5.1直接连接方式测试适配器是则是位于测试用例和待测系统之间的一层。当创建测试适配器时，Cord配置文件中的Action并不是待测系统的方法和事件，而是适配器中的方法与事件；那么生成的测试代码也调用适配器中的方法，期待适配器发起的事件。适配器的作用是把这些方法调用转换为待测系统的方法调用，如图5.2所示。当待测系统是非托管代码实现，或者测试用例与待测系统需要远程通信，或者存在一个中间层用于抽象模型和测试（比如控制待测系统的用户界面）时，这种连接被广泛运用。适配器由于避免了对托管测试代码的依赖，从而极大的增加了specExplorer的适用范围。图5.2测试适配器方式模型开发者与适配器或者待测系统的实现者基于Action的接口规范打成一致，即可并行工作。接口实现只要在需要运行生成的测试代码时能够执行即可。对于模型开发者来说，他们可以先把Action声明成abstract，即可在没有适配器或者待测系统实现的情况下进行建模。5.3静态模型和实例模型SpecExplorer在使用过程中会让用户根据不同的情况选择不同的模型，主要分为2种类型的模型：静态模型和实例模型[14]。前面提到了两种连接测试用例与待测系统的方式：直接连接和适配器连接。如果你决定使用后者，那么适配器本身的设计决定了你选择静态模型还是实例模型。一个静态的适配器可以被用来控制一个基于实例的待测系统，反之亦然。考虑到测试适配器只是整个测试体系中的一个组件，所以这里进行选择的基本原理和设计任何一个面向对象的组件的基本原理是一致的。注意这里并不是一个是或者否的决定，静态和基于实例的Action可以共存于同一个适配器中。Cord脚本中Action的声明被用于连接测试用例与待测系统或者适配器。总的来说，如果你的测试用例是调用待测系统或者适配器的静态方法，那么Action就应该是静态的；如果调用的是待测系统或者适配器的实例化方法，那么Action就是基于实例的。所以选择静态模型还是实例模型的决策权并不在建模者，而在于待测系统或者适配器的设计者。当然，两者可以是扮演不同角色的同一个人。基于实例的Action意味着模型调用某一对象的方法，该对象不仅仅在模型探索阶段存在，在测试运行阶段也是存在的。所以该对象必须是之前某个步骤的输出，如果一个方法创建了一个没有返回的对象，那么显然这一对象不能在模型的后续步骤中被用到。SpecExplorer允许把基于实例的Action与静态的模型方法进行对应（反过来亦可）。虽然一般来说不推荐这么做，因为基于实例的Action对应基于实例的模型方法，静态Action对应静态模型方法是很自然的设计，但是有时建模者不同意待测系统或适配器的设计，而希望用另一种模型设计。我们的目标是尽可能在满足需求的基础上让用户模型更为简单并更容易维护。基于模型的测试的优缺点与其他软件测试技术相比，基于模型的测试有以下优点[15]：SUT的故障检测软件测试的主要目的是发现SUT中的错误，事实证明，基于模型的测试可以很好的检测到故障数目。降低测试成本和时间基于模型的测试在编写和维护模型上花费的时间和精力要低于手工测试中设计和维护一个测试套件的投入成本。提高测试质量手工测试的质量依赖于富有创造力的测试工程师，每个测试用例产生的原因是不会记录的，并且这些测试用例不容易涉及到初始的系统需求。基于模型的测重复化。通过考虑模型的覆盖就可以测量测试套件的“质量”。同时，基于模型的测试相比手动测试可以用来生成更多的测试。通过改变模型的测试选择标准或者告诉工具来生成更多的测试，我们可以很容易地获得非常大的测试套件，这可以帮助发现更多的错误。需求缺陷检测一个有时意想不到的好处是对于非正式的需求，基于模型的测试可以通过编写模型来暴露问题的所在，而这些需求通常是记录在一个大型的、可能包含遗漏、矛盾的、不清楚的自然语言文档中。基于模型的测试的第一步就是通过构建一个抽象模型SUT来澄清这个预期的行为，这个模型要求具有精确的语义，以便它可以分析一个机器。所以建模阶段通常要求公开许多问题。可追溯性可追溯性是能够涉及到模型中每个测试用例，测试选择标准，甚至到非正式的系统需求。可追溯性有助于解释测试用例的生成原因，也可以在模型发展时优化测试执行。例如，当我们使用UML状态机作为建模表示法，测试生成算法会记录模型的哪些转换被用于每个测试用例。需求的演变手工测试中，如果测试设计和系统的需求变化，大量的工作经常需要花费在更新测试套件上来反映新的需求。基于模型的测试可以通过更新模型来重新测试，因为模型通常远小于测试套件，这样就可以花费更少的时间来应对不断变化的需求。并且使用工具分析新旧需求的差异，还可以报告哪些测试不再相关，哪些测试涉及修改后的需求，哪些测试是新加的。所以，一个需求改变后，相应变化的模型可以将测试分为：删除、不变、改变、新增四组。当测试时间有限的情况下，只执行后两组是非常有用的。正是由于基于模型的测试具有诸多优点，可以解决许多其他测试技术不能解决的问题，所以在WEB应用测试、通信协议测试等复杂系统中具有广泛的应用。不过，基于模型测试也不是万能的，也存在一些局限性：1．过时的需求作为一个软件工程的发展，有时非正式的需求变得过时了。如果一些基于模型的测试人员从过时的需求开始工作，他们将建立错误的模型，这样就会在SUT找到大量的“错误”。2．不适当使用基于模型的测试基于模型的测试并不是一颗可以迅速发现程序每个漏洞的子弹，也不会比标准的自动化测试流程更有效或更经济。它的作用是在输入准确的前提下为复杂的项目(比如实时或嵌入式程序设计)实现有实际价值的、非重复性模拟测试。3．分析失败的测试时间当一个生成的测试失败，我们必须决定是否由于SUT、适配器代码或错误的模型引起。基于模型的测试生成测试序列相比手工设计的测试序列可能会更复杂，这就使得发现导致失败的测试更加困难和耗时。4．无用的指标当测试设计，大多数经理使用手动测试用例的数量作为衡量设计测试进展顺利。但基于模型的测试容易产生大量的测试，所以测试数量指标是没有用的。有必要引入其他的测量测试方法，如SUT代码覆盖率，需求覆盖率，和模型覆盖率。参考文献[1]毛澄映,卢炎生.构件软件测试技术研究进展[J].计算机研究与发展,2006,43(8):1375-1382.[2]SchieferdeckerI.Model-BasedTesting[J].IEEESoftware,2012,29(1):14-18.[3]BouquetF,DadeauF,LegeardB,etal.JML-Testing-Tools:ASymbolicAnimatorforJMLSpecificationsUsingCLP.[M]//ToolsandAlgorithmsfortheConstructionandAnalysisofSystems.SpringerBerlinHeidelberg,2005:551-556.[4]HarelD.Statecharts:avisualformalismforcomplexsystems[J].ScienceofComputerProgramming,1987,8(3):231-274.[5]AvritzerA,LarsonB.LoadTestingSoftwareUsingDeterministicStateTesting.[M].ACM,1993.[6]HoornAV,RohrM,HasselbringW.Generatingprobabilisticandintensity-varyingworkloadforweb-basedsoftwaresystems[C]//PerformanceEvaluation–Metrics,ModelsandBenchmarks:ProceedingsoftheSPECInternationalPerformanceEvaluationWorkshop(SIPEW’08),volume5119ofLectureNotesinComputerScience(LNCS.2008:124--143.[7]PooreJH.Introductiontothespecialissueon:model-basedstatisticaltestingofsoftwareintensivesystems[J].Information&SoftwareTechnology,2000,42(12):797-799.[8]MaurerPM.TheDesignandImplementationofaGrammar-basedDataGenerator.[J].SoftwarePractice&Experience,1992,22(3):223-244.[9]PretschnerA,PhilippsJ.10MethodologicalIssuesinModel-BasedTesting[J].LectureNotesinComputerScience,2005,3472:11-18.[10]LamsweerdeAV.Formalspecification:aroadmap.[J].FutureofSoftwareEngineeringAFinkelsteinAcm,2000:147-159.[11]\o"查看此用户资料"xianglims.百度百科SpecExplorer.[EB/OL].[2016-01-18]./link?url=wGJJPEPVVYUNI5dn69s9uJKp1p4iw7FyNtj0TlMZ8eaRDxdt-uWt_tnTIbzJ_IJoS-sKhaMiBqlcgg1BUfa84_.[12]朱永光.用SpecExplorer进行基于模型的测试.[EB/HYPERLINK"/s?wd=OL&tn=44039180_cpr&fenlei=mv6quAkxTZn0IZRqIHckPjm4nH00T1d9rH7WmymYn1Rz