理论计算机科学电子笔记190（2007）33-46www.elsevier.com/locate/entcs处理模型更改：使用模型标记器的Gordon Fraser1，2，Bernhard K.Aichernig3和Franz Woozig4格拉茨科技大学软件技术学院A-8010格拉茨，奥地利摘要最近提出了几种基于模型检查器的测试用例自动生成方法。性能和适用性在很大程度上取决于所使用的模型的复杂性。对于复杂的模型，创建一个完整的测试套件的成本可能很高。如果模型改变了，那么通常测试套件会完全重新生成.然而，只有测试套件的一个子集可能会被模型更改所无效。因此，在这种情况下创建完整的测试套件会因为不必要地重新创建有效的测试用例而浪费时间。本文研究了在模型改变后减少重新创建测试集的方法。这也与回归测试有关，在回归测试中，变更后所需的测试用例的数量应该最小化。本文提出和评估方法，以确定过时的测试用例，并扩展任何给定的测试用例生成方法的基础上，模型检查器，以创建测试用例的测试套件更新或回归测试。关键词：使用模型检查器进行测试，回归测试，测试套件更新，模型更改，自动测试用例生成1引言为了保证软件的正确性，需要有有效的方法，这就产生了许多不同的测试方法。最近，模型检查器已被认为是测试用例生成使用在几个作品。一般来说，利用模型检查器的反例机制来创建可用作测试用例的跟踪。1这项工作得到了FIT-IT研究项目“具有不同安全完整性级别的安全关键分布式嵌入式实时系统（TeDES）的系统测试用例生成"的支持2电子邮件地址：fraser@ist.tugraz.at3电子邮件地址：aichernig@ist.tugraz.at4电子邮件地址：wotawa@ist.tugraz.at1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.08.00434G. Fraser等人/理论计算机科学电子笔记190（2007）33如果用于测试用例生成的模型被改变，这有几个影响。使用模型检查器创建的测试用例是模型的有限执行路径，因此在模型更改之前创建的测试套件可能是无效的。由于使用模型检查器的测试用例生成是完全自动化的，因此显而易见的解决方案是使用更改后的模型创建一个新的测试套件。只要模型的复杂度很小，这是一种可行的方法。如果模型复杂度很高，使用模型检查器可能会导致测试用例生成过程的计算成本很高。然而，并不是所有的测试用例都可能因为模型的改变而许多测试用例对原始模型和修改后的模型都是有效的。在这种情况下，重新创建这些测试用例所花费的时间将被浪费。当识别无效的测试用例并只创建必要的新测试用例时，有潜在的节省。如果一个模型在回归测试场景中发生了变化，在变化之前从模型中派生的测试套件无法检测到任何错误，那么运行一个完整的测试套件可能是不必要的。在这里，运行那些针对模型更改创建的测试就足够了在本文中，我们提出了不同的方法来处理模型的变化。哪种方法更可取取决于具体场景中的总体目标--测试用例生成或测试用例执行的成本是否最小化本文的主要贡献如下：• 我们提出的方法来决定是否一个测试用例是过时的模型的变化，或者如果它仍然有效。这种方法的可用性允许重用旧的测试套件的测试用例，并且是降低新模型的测试用例生成过程的成本的必要先决条件。• 我们提出了不同的方法来创建新的测试用例后，模型的变化。如果在模型变更后执行的测试用例的数量应该最小化，则这些测试用例可以用作回归测试它们也被用来更新用旧版本的模型创建的测试套件.• 实证评估试图回答两个研究问题：（1）与新创建的测试套件相比，测试套件更新对整体质量的影响如何？(2)与在模型更改后完全重新创建测试套件相比，是否有性能增益？本文的组织如下：第2节识别了模型的相关类型的变化，并将它们与具体的模型检查器输入语言相关联，然后提出了我们对识别无效测试用例和创建新测试用例的任务的解决方案。第3节描述了用于评估这些方法的实验设置和测量方法，并给出了这些实验的结果。最后，第4节讨论了结果，并总结了论文。2处理模型更改由于本文考虑的是用模型检查器创建的测试用例，本节回顾了这些方法的基本原理在对模型进行了简短的理论分析G. Fraser等人/理论计算机科学电子笔记190（2007）33350我们使用具体模型检查器的输入语言来呈现处理模型更改的方法。2.1预赛模型检查器是用于形式验证的工具它以自动机模型和时态逻辑属性作为输入，然后有效地探索模型的整个状态空间，以确定模型和属性是否一致。如果检测到不一致，模型检查器返回一个示例执行跟踪（反例），说明如何达到违反状态。基于模型检查器的测试的思想是使用这些反例作为测试用例。近年来，人们提出了几种不同的方法来强制模型检查器创建跟踪模型检查器使用Kripke结构作为模型形式：定义2.1[Kripke结构] Kripke结构M是一个元组M=（S，s0，T，L），其中S是状态的集合，s0∈S是初始状态，T<$S×S是总转移关系，L：S→2AP是将每个状态映射到在该状态下成立的原子命题集合的标记函数。AP是原子命题的可数集合。属性由时态逻辑指定。在本文中，我们使用线性时间逻辑（LTL）[12]。LTL公式由原子命题、布尔算子和时态算子组成。X表示下一个状态。例如，X a表示a在下一个状态中必须为真。 U是until运算符，其中U b意味着a必须从当前状态保持到b为真的其他运算符可以用运算符U和X表示。例如，在一个示例中，G x是<$（true U<$x）的简写，要求x始终为真。LTL的语法如下给出，其中a∈ AP：φ：：= a| ¬φ|φ1∧φ2|Xφ |φ1U φ2| Gφ。如果模型检查器确定一个模型M违反了一个性质φ，那么它返回一个描述该性质违反的跟踪。跟踪是模型执行序列的有限前缀（路径）：定义2.2 [路径]一条路径p：= 0，. Kripke结构M的sn∈ T是一个有限或无限序列，使得对M，n ∈ 0 ≤< in：（si，si+1）∈T.测试用例t是路径p的有限前缀。我们认为这样的测试情况下，预期的正确输出。这种测试用例被称为通过或肯定测试用例。测试用例生成的结果是一个测试套件。由于模型检查器创建的测试用例是线性序列，它们不能解释被测系统的非确定性行为。因此，我们限制了确定性模型的结果。基于模型检查器的测试的主要应用领域是反应系统，其中输入以循环方式处理，并且相应地设置输出值。定义2.3[无效测试用例]模型M=（S，s0，T，L）的测试用例t为如果满足以下任何条件，则对修改后的模型MJ=（SJ，sJ，TJ，LJ无效是真的：36G. Fraser等人/理论计算机科学电子笔记190（2007）33J我：<... ，si，si+1，. . >=t<$（si，si+1）∈/TJ（一）我：<...，si，. >= t L（si）L（si）（2）J我：<... 我... . >=t（si∈/S）（3）实际上，Kripke结构是用模型检查器的输入语言描述的。这种输入语言通常通过定义AP上的条件来描述转换关系，并根据这些条件设置变量的值转换条件C描述了一组状态Si，其中C是满的。在这些状态的所有后继状态中，变量v必须具有下一个值n：s∈Si：L（s）|= CsJ：（s，sJ）∈T→“V = N“∈ L（S J）. 在本文中，我们使用模型检查器NuSMV的语法[6]。清单1显示了NuSMV模型中的转换关系。Kripke结构中的变化由模型源中的语法变化这样的变化可以被自动检测，语法树的比较。我们只对不会使完整测试套件失效由模型检查器创建的轨迹仅由状态s组成，使得对于模型源中定义的每个变量v，存在命题S. 例如，在模型源中添加或删除变量将导致对于S中的每一个状态，L的变化，因此会使在变化之前创建的任何测试套件无效。因此，有趣的变化类型是那些应用于模型描述中变量的下一个状态的转换条件或值的变化。分配next（var）：= case条件1：nextvalue1;条件2：nextvalue2;esac;清单1：SMV文件的ASSIGN部分。init（x）：= 1;next（x）：=casereturn0：0;1：1;1：x;esac;清单2：t：=（x = 1），（x = 0），（x =1）.2.2识别Objective测试用例为了使用模型检查器来决定测试用例对于给定模型是否有效，测试用例被转换为可验证的模型。如Ammann和Black [1]所建议的那样，所有变量的转移关系被给出，使得它们依赖于一个特殊的状态计数变量。 清单2中建模了一个示例转换关系，其中State表示状态计数变量。有两种方法可以判断模型改变后测试用例是否仍然有效。一个是基于一次处决测试用例在模型上的属性，而其他验证变量在测试用例模型上改变相关属性。G. Fraser等人/理论计算机科学电子笔记190（2007）3337符号测试用例执行：模型检查器对于符号执行并不是严格必要然而，在基于模型检查器的测试用例生成的场景中，使用模型检查器的可能性是方便的通过将实际模型添加为测试用例模型中实例化的子模型，可以使用模型检查器对测试用例进行符号执行作为子模型的输入变量最后，通过验证声称测试用例和子模型的输出值在测试用例的长度上相等的属性，模型检查器确定是否确实如此：MONITORINGCHANGED_MODEL（inputvariableles）变更模型MOST主测试用例模型VARSubMode1：changed_mode1（inputvars）;SPECG（状态<最大状态->输出=子模式1。输出）清单3：测试用例的符号执行。现在，检查一个测试套件关于一个改变的模型的有效性的问题减少到模型检查每个测试用例与新的模型相结合。每个导致反例的测试用例都是过时的。没有导致反例的测试用例仍然有效，因此不受模型变化的影响。这种方法的一个缺点是，实际的模型涉及到模型检查。如果模型很复杂，这可能会对性能产生严重影响。更改属性：在许多情况下，测试用例模型可以简单地针对某些属性进行检查这避免了在模型检查过程中包含新模型如果一个转换条件或目标被改变，那么改变的转换可以被表示为一个时态逻辑属性，这样任何在新模型上有效的测试用例模型都必须满足这个属性：G（改变的条件→X变量=改变的值）这样的更改属性可以从模型检查器模型源文件中自动创建具体方法取决于模型检查器使用的语法如果变量转换被移除，则只能确定测试用例是否使用否定属性来获取旧转换：G（旧条件→X<$（变量=旧值））38G. Fraser等人/理论计算机科学电子笔记190（2007）33任何采用旧转换的测试用例都会导致反例。从理论上讲，如果被移除的转换被包含或替换为另一个行为相同的转换，则后一种情况可能会报告误报这可能是手动编辑模型的结果这种误报可以通过针对该更改属性检查新模型来只有当这导致一个反例时，删除才有效果，并且确实需要在测试用例上进行检查。虽然使用完整模型的验证是必要的，但与符号执行方法相比，它只需执行一次当测试关于模型变更的实现时，被模型变更无效的测试用例可能是有用的。明显阳性的测试用例可以用作阴性回归测试用例。负测试用例是这样一种测试用例，它可能不会被正确的实现通过因此，通过负回归测试用例的实现遵循旧模型描述的行为。2.3创建新的测试用例一旦模型改变后的过时测试用例被识别并丢弃，剩下的测试用例就是那些只执行未改变行为的测试用例。这意味着通过更改添加的任何新行为都不会被测试。因此，必须创建新的测试用例。调整Objective测试用例：对旧测试套件的分析识别出包含已更改行为的测试用例。新的测试用例可以通过在改变的模型上执行这些测试用例来创建，记录新的行为。这是通过将测试用例模型和更改后的模型结合在一起（如第2.2节所述），使用模型检查器完成的。测试用例模型包含状态计数器State和最大值MAX。模型检查器使用属性G（State<$MAX）进行查询。这实现了其中State的值增加到MAX的跟踪。修改后的测试用例只是由该跟踪中更改后的模型的值分配或者，当使用符号执行方法检查测试用例时，该过程中的反例可以直接用作测试用例。与刚才描述的方法相比，根据更改，生成的测试用例可能会更短。理论上，这会对新测试套件的整体覆盖率产生负面影响。这种方法的缺点是，如果没有相关的过时的测试用例，更改后的模型可能包含无法覆盖的新行为。在评估中，我们将这种方法称为适应。选择性地创建测试用例：Xu等人[13]提出了一种使用模型检查器进行回归测试的方法，其中一个特殊的比较器从两个版本的模型中创建陷阱属性一般来说，基于陷阱属性的测试用例生成方法表达了测试用例中的项目G. Fraser等人/理论计算机科学电子笔记190（2007）3339构成覆盖率标准的属性声明无法达到的项目[9]。例如，一个陷阱属性可能会声明某个状态或转换永远不会到达。当根据陷阱属性检查模型时，模型检查器返回一个可以用作测试用例的反例。我们推广了Xu等人的方法，以便适用于更广泛的测试用例生成技术。大多数方法通过创建一组陷阱属性或通过创建模型的突变体来工作。对于所有使用陷阱属性的方法，我们简单地计算陷阱属性集的差异，作为一种替代方案，需要一个特殊的比较器用于特定的规范语言和覆盖标准。原始模型产生一组属性P，而改变后的模型产生PJ。新的测试用例是通过针对Pj-P中的所有属性对更改后的模型进行模型检查来创建的。集合差异的计算不需要对给定的测试用例生成框架进行任何调整。此外，它还适用于不基于覆盖标准的方法，例如，布莱克提出的方法[4]。在这里，属性是通过将所产生的特性发生突变，突变体用作陷阱特性。可以想象，这种方法可能无法保证达到一定的覆盖标准，因为对于某些可覆盖的项目，相关的测试用例是无效的，即使项目本身没有被更改所影响。如果需要某个标准的最大覆盖率，则另一种解决方案是针对新模型的陷阱属性集对测试用例模型进行模型检查，而不是选择集差。为了简单起见，我们考虑在本文中使用集合分类的直接方法在评估中，我们将此方法称为Update。第二类测试用例生成方法使用模型的突变体来创建测试用例（例如，[3、2、11、8]）。例如，状态机复制[11]结合了原始模型和突变模型，使它们共享相同的输入变量。然后查询模型检查器是否存在模型和突变体的输出值不一致的状态在这里，解决方案是只使用那些与模型变化相关的突变体。为此，确定改变的位置（例如，在通过解析模型创建的语法树中），然后过滤改变的模型的突变体的全集，使得仅保留NuSMV源中改变的语句的突变体。测试用例生成只使用剩余的突变体。专注于模型更改的作为第三种方法来创建变更相关的测试用例，我们提出了一个通用的扩展适用于任何测试用例生成方法。它在调用模型检查器之前重写模型（或其变体）和测试用例生成中涉及的属性。 这种重写是完全自动化的。 该模型是前-由一个新的布尔变量改变。如果有多个变化，那么每个变化都有一个变量：变化i。这些变量初始化为40G. Fraser等人/理论计算机科学电子笔记190（2007）33值为false。当达到采取改变的转换的状态时，改变变量被设置为真。一旦一个变量为true，它就保持这个值。变更变量的转换关系由变更变量的转换条件组成，如清单4所示。MONITOR主VARtranslate：boolean;...分配init（changed）：=FALSE;next（changed）：= case更改代码：TRUEE;1：已更改; --默认分支esac;next（changngedvar）：=case更改条件：更改值;...清单4：带有特殊变量的转换关系表示变化。重写测试用例生成方法中涉及的属性，以创建专注于模型更改的测试用例。作为一个例子，我们使用LTL，虽然转换也可以应用于计算树逻辑（CTL）[7]。定义2.4[变化变换]LTL属性φ的变化变换φJ=α（φ，c）相对于布尔变量识别的变化，表c，其中a∈AP作为一个命题公式，递归地定义为：α（a，c）=a（四）α（<$φ，c）=<$α（φ，c）（五）α（φ1<$φ2，c）=α（φ1，c）<$α（φ2，c）（六）α（Xφ，c）=X（c→α（φ，c））（七）α（φ1U φ2，c）=α（φ1，c）U（c→α（φ2，c））（八）基本上，所有的时态运算符都被重写，以包含对变化变量的含义。这实现了仅创建包括改变的转变的这种反例。对于多个更改，每个更改必须有一个修改版本的每个属性，以确保所有更改都得到平等的测试。在评估中，我们将此方法称为Focus。3实证结果上一节介绍了在基于模型检查器的测试用例生成场景中，不同目标的不同可能性，以应对本节试图评估这些想法的可行性。首先，进行G. Fraser等人/理论计算机科学电子笔记190（2007）3341的描述，然后提出和讨论的结果。3.1实验装置本文描述的方法已经使用编程语言Python和模型检查器NuSMV [6]实现所有实验都在具有Intel Core Duo T2400处理器和1GB RAM的PC上运行，运行GNU/Linux。我们自动识别两个版本的模型之间的变化，通过分析的抽象语法树从解析模型。我们使用基于Kirby等人[10]的版本的巡航控制应用程序的简单为了评估所提出的方法，突变得分和创建时间的新的和更新的测试套件进行了跟踪，在几个变化。 选择不代表真实变化的变化会威胁到实验的有效性。因此，实验在不同变化下进行多次，并将所得值平均。在第一步中，突变体是从假定正确的模型中产生的。使用了以下突变算子（详见[5]）：STA（replace atomic proposals with true/false），SNO（negate atomicproposals），MCO（remove atomic proposals），LRO，RRO，ARO（logical，relational and arithmetical operator replacement，respectively）.分析所得突变体以消除等效突变体。这是通过状态机复制方法的变体[11]来完成的，其中模型检查器被询问是否存在模型的输出值及其突变体的状态。如果没有返回反例，则检测到等效突变体。通过对照需要一些基本行为的一组基本性质检查每个突变体，进一步减少突变体的集合，例如，一些重要国家的可达性从产生的不等价突变体集合中随机选择一个突变体使用该突变体，重复该过程，直到实现20个可见模型变化的在20个这样的序列上进行实验，并对结果进行平均。对于模型版本的每个序列，执行以下操作：从包含所有20个更改的模型开始，使用方法转换覆盖标准（NuSMV模型的每个转换条件一个测试用例）创建测试套件，反射转换关系的突变[4]和状态机复制[11]。之所以选择这三种方法，是因为它们应该代表大多数类型的可设想的方法。然后，选择模型的下一个版本，并分析先前模型的测试套件中的过时测试用例，并创建新的和更新的测试套件。然后计算所有这些测试集的突变得分。突变评分是识别的突变体与突变体总数的比率。它是通过对突变模型象征性地执行测试用例模型来计算的。对每个模型版本重复此过程，直到原始模型。42G. Fraser等人/理论计算机科学电子笔记190（2007）331008060402000 5 10 15 20变化(a)突变评分1.41.210.80.60.40.200 5 10 15 20变化(b) 创建时间Fig. 1.转换覆盖测试用例生成。表1唯一新测试用例的平均数量。测试套件类型充分适应更新重点过渡5.7511.46.6反射19.352.57.0524.4SM复制33.352.856.4529.43.2结果图1-3（a）显示了不同模型版本过程中不同方法的突变评分。对于适应和更新方法，存在突变得分的退化。退化随着每个模型的变化而增加，因此当使用这种方法时，建议在一定数量的变化之后创建新的测试套件。相比之下，改变焦点方法实现的突变分数有时甚至高于全新测试的突变分数-完全适应更新重点完全适应更新焦点%突变评分时间（秒）G. Fraser等人/理论计算机科学电子笔记190（2007）33431008060402000 5 10 15 20变化(a)突变评分60504030201000 5 10 15 20变化(b) 创建时间图二. 反射转换关系的突变。套房.这是因为使用焦点方法创建的测试套件比转换覆盖标准的新测试套件更大。适应通常实现最低的突变分数。然而，突变得分仅略小于更新方法，因此显著的性能增益可以证明这种降级是合理的。图1-3（b）显示了创建和更新测试套件的计算时间.所有方法都比完整的测试用例生成过程快。在大多数情况下，测试套件适配的执行速度明显快于所有其他方法。自适应的性能取决于模型的复杂性和无效测试用例的数量，因此对于实验中的所有测试套件都是相似的。相比之下，更新和聚焦方法的性能取决于它们所基于的测试用例生成方法。对于像转换覆盖聚焦这样的简单方法，它是非常有效的，而随着测试用例生成复杂性的增加，性能增益较小。对于实验中使用的最复杂的方法（基于状态机复制），完全适应更新重点完全适应更新焦点%突变评分时间（秒）44G. Fraser等人/理论计算机科学电子笔记190（2007）331008060402000 5 10 15 20变化(a)突变评分40353025201510500 5 10 15 20变化(b) 创建时间图三.通过状态机复制生成测试用例。与创建一个新的测试套件相比是最小的。最后，表1比较了每次模型更改后平均创建的新测试用例的数量这个图表揭示了为什么改变焦点方法获得如此高的突变分数：生成的测试用例的数量明显高于任何其他方法。有趣的是，它甚至比使用转换和反射方法为新的测试套件生成的测试用例的数量更高，尽管测试用例生成的平均速度仍然更快。4结论在本文中，我们已经展示了如何决定一个测试用例是否仍然有效后，它被创建的模型被改变。 这样，就有可能在模型更改后重用一些测试用例，并减少测试套件生成的时间。提出了创建特定于模型变化的测试用例的不同方法我们在实验中使用了模型检查器NuSMV，并将其作为示例模型完全适应更新重点完全适应更新焦点%突变评分时间（秒）G. Fraser等人/理论计算机科学电子笔记190（2007）3345语法.然而，没有理由认为这种方法不适用于其他模型检查器。实验表明，所提出的方法可以用来更新后的模型变化的测试套件，虽然有一个性能提高和质量损失之间的权衡。一般来说，基于模型检查器的方法的主要问题是性能。如果模型太复杂，那么测试用例生成将花费很长时间，甚至可能是不可能的。因此，重要的是找到优化方法的方法。在模型更改后重新创建测试套件时，潜在的节省是显著的。即使对于我们评估中使用的小模型，当仅选择性地为模型更改创建测试用例时，也可以观察到较大的虽然模型通常比它所代表的程序更抽象，但模型的大小仍然很重要。例如，自动转换（例如，Matlab State（SMV）可以产生复杂的模型。所提出的方法以最小的计算量生成新的测试用例，取得了良好的效果。我们不能断定一种方法是更好的，因为更好的方法取决于具体的情况。如果主要目标是最小化重新测试的成本，那么只要没有太多和重大的变化，旧的测试用例的适应是有效的。如果最大化检测与变更相关的故障的可能性更重要，则创建关注变更的测试用例的方法是优选的。例如，在安全相关的场景中，测试套件质量的下降是不可接受的。最后，只为更改的部分创建测试用例的更新方法似乎是一个很好的折衷方案;它降低了成本，同时质量下降不太剧烈。按照Xu等人的思想，使用任何提出的方法创建的测试用例都可以用作回归测试套件[13 ]第10段。有一些方法显式地使用规范属性来生成测试用例[3，11，2]。本文没有明确地涵盖测试套件更新与规范属性有关的方面。然而，测试套件焦点的想法直接适用于这样的方法，以及测试套件更新技术。巡航控制示例只是一个小模型，我们实验中涉及的更改是自动生成的。这足以说明该方法的可行性。然而，更复杂的模型和现实的变化的实际性能测量将是可取的。引用[1] Ammann，P. and P. E. Black，A Specification-Based Coverage Metric to Evaluate Test Sets. HASE239-248。[2] Ammann，P.，W. Ding和D.徐，使用模型测试安全性能，在：第七届复杂计算机系统工程国际会议论文集（ICECCS 2001）（2001），pp. 212-221.[3] Ammann，P.E.，P. E.布莱克和W. Majurski，使用模型检查从规范生成测试，在：第二届IEEE形式工程方法国际会议46比54[4] 布莱克，体育，建模和编组：从模型的反例进行测试，在：第19届数字航空电子系统会议集，2000年，pp.1.B.3-1-1.B.3-6第1卷。46G. Fraser等人/理论计算机科学电子笔记190（2007）33[5] 布莱克，体育，Okun和Y. Yesha，Mutation Operators for Specifications，ASE81比88[6] Cimatti ， A. ， E. M. 克 拉 克 角 ， 澳 - 地 Giunchiglia 和 M. Roveri ， NUSMV ： A New Symbolic ModelVerifier，in：CAV495-499[7] Clarke，E. M.和E. A.陈文辉，应用分支时间时序逻辑设计与合成同步框架，载于：程序逻辑，工作坊（1982），页. 52比71[8] Fraser，G.和F. Woetman ，Property Relevant Software Testing with Model-Buckers，ACM SIGSOFTSoftware Engineering Notes31（2006），pp. 1-10。[9] Gargantini，A.和C. Heitmeyer，使用模型检查从需求规范生成测试，在：ESEC/FSE第七届ACM SIGSOFT软件工程基础研讨会，计算机科学讲义1687（1999），第1687页。146比162[10] Kirby，J.，汽车巡航控制和监控系统的NRL/SCR软件要求示例，技术报告TR-87-07，王研究生院（1987年）。[11]Okun，V.，P. E.布莱克和Y. Yesha，使用Model 100进行测试：确保故障可见性，载于：N。E. Mastorakis和P. Ekel，编辑，2002年WSEAS系统科学国际会议论文集，应用数学计算机科学和电力工程系统，2003年，第100页。公元1351- 1356年。[12] Pnueli，A.，程序的时序逻辑，在：FOCS46比57[13] 徐 ， L. ， M. Dias 和 D. Richardson ， Generating regression tests via model checking ， COMPSAC336-341。
我的内容管理
展开
