理论计算机科学电子札记95（2004）53-62www.elsevier.com/locate/entcs测试无限状态机扩展抽象Marie-Claude Gaudel玛丽-克洛德·戈德尔1，2L.R. IUniversit'edeParis-SudandCNRSOrsay，法国摘要基于形式规格说明的测试已经有了很多研究，特别是在通信协议领域。大多数方法都以被测系统所需行为的有限模型为起点，例如有限状态机。本文讨论的问题时，规范的基础模型是不有限的。关键词：软件测试，有限状态机，无限测试机，测试推导。1介绍有很多关于基于正式规范的测试的研究，特别是在通信协议领域。大多数方法都以被测系统所需行为的有限模型为出发点，例如有限状态机（FSM）[8]或有限标记转换系统（LTS）[2]。[1]非常感谢格雷戈里·莱斯蒂恩（Gregory Lestiennes）对本文所述观点的大量讨论和贡献。我也非常感谢C NR S“T e c h ni que s A van c ′ ee s de T e st“的具体研究行动的成员，他们为我提供了两次成功和有效的工作。2 电子邮件地址：mcg@lri.fr1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.04.00554M.- C. Gaudel / Electronic Notes in Theoretical Computer Science 95（2004）53-本文讨论了当底层模型的规格是不确定的。 一旦在操作和保护中使用了非平凡的数据类型，就像在完整的LOTOS中，在UML状态图中，在CCS或CSP中扩展了值传递的可能性，如CSP-Casl等。这里，在[6]和[9]的行中描绘了一些解决方案。 它们基于为测试有限行为模型而开发的方法和为数据类型规范而开发的方法的一些集成[1]。本文的组织如下：第2节回顾了基于规范的测试的一些概述;第3节简要介绍了有限模型的测试推导;第4节介绍了抽象数据类型的测试推导基础;第5节介绍了扩展模型，第6节给出了基于此类模型的测试提示。2基于规格说明的测试概述本节简要回顾了一致性测试的主要概念的定义什么是一致性测试的一般定义是，它旨在通过以下方式验证系统是否满足其规范• 基于规范的某些测试集的构造，• 将这些测试提交给被测系统，• 观察他们的处决和判决声明（神谕）的基础上的具体说明。一个中心概念是被测系统SUT对特定SP的满足度的定义。让我们注意SUT sat SP这个关系。实际上，它不是系统本身和规范之间的关系，因为它们在本质上太不同了。它是模型之间的关系，即SUT的某个模型和规范给出的某个模型。在测试领域存在着几种这样的关系。这种关系的例子，其中的模型是标签转换系统，或一些变种，是conf或ioco关系[13]。模型是异质代数的其他关系是基于代数对属性的观测满足的一些概念[1][10]。这种满意度关系被用作测试集的定义和与规范相关的判决的基础。这样的定义应该确保通过测试集的实现满足规范。一般来说，要得到这个属性，需要对实现的类引入一些合理的限制。这些限制被称为测试假设，或可测试性假设[4]，[1]，[2]。他们通常很虚弱。例如，它们排除了恶魔般的非确定性实现，M.- C. Gaudel / Electronic Notes in Theoretical Computer Science 95（2004）53-55在测试过程中会表现正确，而在测试之后会表现不正确。他们确定了测试将给出有意义结果的实现然而，在一致性测试中还有另一个更强的假设，即实现的行为就像用于一致性关系的那种模型。这个假设并不总是像它应该的那样被仔细考虑（例如关于动作的原子性在这些假设下，给定一致性关系，就有可能从一个规范中导出一组测试和一个确保满意的结论。这样的测试集被称为完全[2]或穷举[1]。不幸的是，这一套通常是有限的或太大，在实践中提交。因此，我们需要选择它的一个适当的有限子集有各种方法来选择这样的测试子集。 三在基于规范的一致性测试的框架中，最已知的测试选择方法是：• 覆盖标准，• 选择假说，• 测试目的。最常用的覆盖标准是基于规范的模型显然，这取决于模型的类型。一个众所周知的例子[4]在有限状态机的情况下，是转换覆盖。另一种方法是基于加强执行假设的想法。例如，让我们考虑经典的分区测试策略（更确切地说，子域测试策略）。它包括从规范中导出覆盖穷举测试集的子集（可能不相交）的集合。然后选择每个子集的元素并提交给测试中的实现。这种选择假设被称为一致性假设：假设SUT在测试子集上的行为是一致的。从代数规范导出均匀子域是通过LOFT工具实现的[11]。另一种方法是通过有限数量的测试目的来选择测试，这些目的描述了一些被认为对测试很重要的行为。使用规范和测试目的，生成测试用例。这种选择用于具有输入和输出的LTS的TGV工具[7]中。3有限模型在这种情况下，有限模型是通过一些有限的状态集合来描述系统的行为，以及从状态到状态的一些转换，56M.- C. Gaudel / Electronic Notes in Theoretical Computer Science 95（2004）53-一些有限的字母表。有限模型有许多变体，这取决于标签的性质以及与标签相关的环境交互的类型非常粗略地说，在有限模型测试领域有两类方法。第一个来自电路和交换系统文献，这是历史上第一个解决这些问题的文献。然后，它被应用于程序（见[8]的调查）。底层模型是Moore机或Mealy机。输入和输出（或刺激和反应）有明确的概念。实际上，满足关系是SUT的行为就像某种与规范等价的FSM。因此，这种关系是对称的，这意味着SUT和规范之间没有抽象级别的差异。毫无疑问，这里涵盖了这一领域极其丰富的成果和方法。让我们假设测试是输入序列，即特定FSM的底层图中的路径。图算法被广泛用于测试推导。主要的覆盖标准是每个过渡的覆盖。结果表明，在可测性假设下，该方法给出了完整的测试集，即SUT可以由确定性有限状态机建模。这个假设对于（大多数）电路和开关系统以及某些程序类来说是相当合理的。这意味着在给定的状态下，系统对给定输入的反应与系统的先前历史无关。这导致了完整性结果，因为一个成功的转换测试意味着该转换在任何上下文中都将正确运行。一个主要的问题是找到一种方法来确保测试将使SUT处于与要测试的转换的原始状态等效的状态，然后提供一种方法来检查结果状态是否是转换的目标状态。可以通过一些额外的输入来观察这些状态。根据特定的FSM，足够的观测可能基于所谓的可区分序列，特征集等。第二种方法主要是为了测试通信协议而开发的（参见[2]的注释书目），并且受到进程代数的一些理论发展的强烈影响[12]。协议规范的控制部分被建模为有限标记的转换系统，或者输入和输出动作被区分的一些变体，或者...上面的某种FSM（研究方法的分类是一项艰巨的工作......）.提交测试包括与测试人员并行运行SUT，并观察所执行的操作和死锁。测试人员是精心设计的过程，有一组与SUT相对应的动作，M.- C. Gaudel / Electronic Notes in Theoretical Computer Science 95（2004）53-57通过成功和失败的特殊行动来丰富存在几种满意关系，它们远非等价关系，例如，允许实现比规范更具确定性，或者比规范更少阻塞。最流行的是ioco关系[13]，其中输入和输出标签是不同的。它与可测试性假设相关联，即实现是输入使能的，即它接受任何状态下的任何输入。ioco关系要求在实现可执行的规范的任何跟踪之后，实现的可能输出集合包含在规范的可能输出集合[13]中给出了ioco的完整测试集，并在[9]中进行了改进（即简化）。TGV工具基于这种满意度概念。4抽象数据类型我们在这里考虑数据类型的代数规范。它们有两个部分：一个签名n=（S，OP），其中S是一个有限的排序集，OP是S中排序上的一个有限的操 作 名 集 ， 以 及 Ax ， 一 个 有 限 的 公 理 集 。 如 果 SP 是 一 个 规 范（Specification，Ax），SUT是某个针对SP进行测试的系统，我们假设SUT提供了某种方法来执行SP的操作：例如，它是一个类，其接口对应于规范的签名。 SUT对SP的测试是Ax中某个公理的基础实例化。测试实验包括通过SUT评估测试中出现的项，并检查结果值是否满足原始公理表示的属性。这一思想首先在[5]中对方程提出，然后在[1]中推广到正条件公理，然后在[10]中推广到任何一阶公理。模一些可测性假设和一些可观测性约束，公理的所有基础实例的集合是一个穷举测试集。在大多数情况下，它显然太大而无法使用，需要一些选择方法。规范的文本为选择提供了非常有用的指导。对于代数规范，这些准则依赖于公理的覆盖范围，并结合运算定义中出现的情况。这是一个经典的技术称为展开[3]。这些原则使得有可能自动建议均匀性假设，并通过展开的数量来调整它们的强度，以满足SUT所需的质量。让我们以优先级队列上的get操作的具体化为例。此操作返回非空队列中具有最高优先级的消息，并在队列58M.- C. Gaudel / Electronic Notes in Theoretical Computer Science 95（2004）53-空的它可以由下面的四个条件公理定义：get（emptyq））=（0.<>）;{0是最弱优先级，<>是空文本} get（add（M，emptyq））=M;isEmpty（Q）=false优先级（get（Q））ge优先级（M）=> get（add（M，Q））= get（Q）;isEmpty（Q）= false优先级（get（Q））lt优先级（M）=> get（add（M，Q））= M;这些公理的覆盖需要四个测试。这些测试对应于三个一致性假设：一个用于大小为1的队列中包含的消息;两个用于大小大于1的队列。更准确地说，只有一个测试用于最后一个输入的优先级小于或等于队列中所有消息的情况，还有一个测试用于最后一个输入的优先级大于队列中所有消息的情况。可以通过展开ge的指定来削弱第二个假设（这里没有给出，但通常有两种情况），将均匀性子域分为最后一个输入的优先级等于队列中的最大优先级的子域和严格小于最大优先级的子域。这种可能性以及其他几种可能性已经在LOFT工具中自动化[11]。值得注意的是，展开的使用并不局限于由公理集定义的运算的测试。最初，展开被定义为分解算法递归程序。Fig. 1. 扩展模型的例子。5扩展模型：在FSM在实践中，大多数系统处理某些数据类型的值。在关联描述中，这些值与表示状态的变量相关联。变量用于外部交互;它们制约某些转换的触发;它们可以在触发转换时通过某些操作进行更新图1中给出了一个示例的一部分，使用了一种接近UML的M.- C. Gaudel / Electronic Notes in Theoretical Computer Science 95（2004）53-59国家图表一个非常相似的例子在[9]中完全呈现。在图1中，M变量是给定类型的Message;每条消息都有优先考虑Q变量的类型为优先队列。 在上一节中已经给出了在这样的队列上的getBuffer（Q）和ClientReady（Q）是状态的类别，具有尽可能多的Q值的状态。它们被称为象征性国家。以类似的方式，符号转换表示转换的类别：对应于转换{|q ∈ Queue}。图2给出了与图1的扩展模型相关联的模型的初始部分的概念。在这里，没有更多的变量，所有的值都被枚举。图二. 基础模型如果可能消息的数量没有界限，并且如果队列没有界限，那么对应于这个状态图的模型是无限状态机，或者无限标记系统。实际上，在真实的例子中，类型是有限的，但可能有非常大的值集，使得底层模型如此之大，以至于必须使用符号标记和方法。有时可以将这些值合并到大的等价类中，以获得有限的模型。但是这里有几个陷阱：生成的模型可能是不确定的（在某些情况下这是可以接受的这对于模型检查和测试推导来说都是一个严重的问题。不可行路径是结构测试中一个经典的麻烦来源，我们在这里面临着它：在一个转换序列上可能有矛盾的守卫60M.- C. Gaudel / Electronic Notes in Theoretical Computer Science 95（2004）53-此外，在协议规范的情况下，转换系统的并行组成和同步问题使故事更加复杂，因为取决于变量的值，某些状态可能拒绝或不拒绝某些动作。然而，扩展模型具有一些优势。由于变量的存在，状态比经典模型更容易观察。这在测试时很重要。6无限模型显然，选择是测试扩展模型的关键问题。但是覆盖标准和选择假设很难在庞大的基础模型上使用。必须以扩展模型为基础。有必要同时考虑到行为描述，这是一个图形，并在测试选择过程中标记转换的操作的属性。统一过程和数据类型测试的第一种方法在[6]中提出，并在[9]中进行了扩展它基于有限长度的符号路径的覆盖（为了得到有限的测试集），通过展开在守卫中发生的操作（为了捕捉有趣的子情况和极限值）来丰富。一旦选择了一条符号路径，就通过符号求值技术构造谓词，该谓词这个谓词是沿着路径遇到的守卫（或条件）的结合，在变量修改的函数中充分更新。 然后通过约束求解得到试验数据。如果这条路是可行的。这种方法有一些缺点。路径长度的界的选择是困难的。在某些情况下，有必要有一个大的边界来覆盖规范的某些特殊部分。这会导致非常大的测试集，并带有无用的冗余。因此，必须考虑扩展模型的较弱覆盖标准一个很好的候选者是符号转换的覆盖。让我们考虑一下象征性的转变图1. cover是什么意思第一个想法是选择一个任意的过渡，对所有优先级队列进行一致性假设然后，它仍然要构建一个跟踪，导致状态ClientReady（q），然后测试程序进程沿着这个跟踪驱动SUT，直到触发转换，然后执行一些检查，以确保结果状态是预期的状态。测试器M.- C. Gaudel / Electronic Notes in Theoretical Computer Science 95（2004）53-61可能涵盖几个象征性的过渡，甚至所有的，如果这样的“旅游”存在。然而，这种选择策略可能会忽略一些有趣的情况。回到get操作的规范（以及remove操作的规范，这是类似的，但在这里没有给出），这个规范表达了指定缓冲器的一个关键方面，即消息按照其优先级进行传递。展开get给出了四种类型的转换来测试所考虑的符号转换：），Buffer（emptyq）>，，，其中isEmpty（Q）=false优先级（get（Q））ge优先级（M），其中isEmpty（Q）= false_。实际上，这定义了对应于要覆盖的符号转换的转换类的划分。这种“符号转换覆盖+展开”的概念它很可能比单独测试规范的数据类型和控制方面的策略具有更好的故障检测能力。在这里给出的例子中，数据类型是以公理的方式定义然而，如上所述，当以算法递归形式描述数据类型的操作时，展开也是可用的请注意，上面的第一个子情况是不可达性的一个很好的例子：，状态ClientReady（emptyq）是不可到达的，因此也是上述的第一个transi- tion。一般来说，检测这种不可达性是不可判定的，就像在结构测试中检测不可行路径一样。在最后一节中，提出并讨论了从无限状态机导出有限测试集的一些策略。很明显，它们必须同时考虑规范的图形部分和逻辑（或算法）部分。一般来说，完全自动化的测试推导是不可行的，因为一些不可判定的结果。然而，使用足够强大的约束求解器和定理证明器可以极大地帮助这个过程，并为有趣的工具提供基础。62M.- C. Gaudel / Electronic Notes in Theoretical Computer Science 95（2004）53-引用[1] Bernot，G.，M.- C. Gaudel和B.李文，基于形式规格说明的软件测试，软件工程学报，1991年，第6期，第387[2] Brinksma ， Ed ， and Jan Tretmans ， Testing Transition Systems ： An AnnotatedBibliography，MOVEP 2000 Summer School，LNCS 2067（2001），187[3] 伯斯托尔河M.，和J. Darlington，A Transformation System for Developing RecursivePrograms，JACM24，1，（1977），44[4] Chow，T.美国，Testing Software Design Modelled by Monte-State Machines，IEEETransactions on Software Engineering，3，4（1978），178[5] Gannon，J.，P. McMullin和R.陈晓，数据抽象实现，规范与测试，计算机程序设计语言与系统学报，1981年，第3期，第211-223页。[6] Gaudel，M. -C.和P.R. James，测试代数数据类型和过程：计算的统一理论形式方面，10，5-6（1999）436[7] Jard，C.，和T. Jron，TGV：理论，原理和算法第六届世界集成设计过程技术会议（IDPT[8] Lee，D.，和M.杨明，有限状态机的测试原理与方法-IEEE调查会议录，84，8（1996），1090[9] 李国忠，软件可靠性工程，2002年第13届IEEE国际软件可靠性工程研讨会（ISSRE-2002），北京，（2002），3[10] 马查多，帕特里夏·D L.， 对甲骨文解释测试结果对代数规范，AMAST[11] 马雷，布鲁诺，LOFT，一个从代数规范中辅助选择测试数据集的工具，TAPSOFT[12] de Nicola，R.，和M.陈文辉，计算机科学与工程，第一卷，第二卷，第一章，第11[13] 张文，输入、输出及重复性静态测试之产生，国立成功大学计算机科学研究所硕士论文，1996年
我的内容管理
展开
