基于模型的多范式自动测试构造技术

理论计算机科学电子笔记111（2005）137-160www.elsevier.com/locate/entcs多范式模型作为自动测试构造Victor V. Kuliamin维克多·库利亚明1，2俄罗斯科学院系统编程研究所（ISPRAS），B. Communisticheskaya，25，莫斯科，俄罗斯联邦http：//www. 伊斯普拉斯。ru/groups/rv/rv.HTML摘要本文讨论了基于模型的测试构造问题以及使用不同类型的模型（操作、契约、公理和基于历史的规范）解决这些问题的方法。 其主要思想是，基于模型的技术具有不同的潜在形式的集成可以给出有价值的实际结果，在测试建设。UniTesK测试开发技术的成功应用说明了这一想法，该技术基于用于描述系统行为的合同规范和用于测试序列生成的操作模型的组合。UniTesK是由ISP RAS的RedVerst [1]小组根据在多个工业软件测试项目中获得的经验设计的。保留字：基于模型的测试，基于规范的测试1介绍在当今世界，越来越多的关键人类活动正在落入软件的控制之下。这种情况需要有效的方法来确保高水平的软件可靠性和其他方面的质量。测试是最有用的质量检查方法之一。但是随着软件复杂性的增长，对软件进行彻底测试所需的时间似乎也按照某种非线性规律增长1这项工作部分得到了RFBR资助02-01-00959，俄罗斯科学支持基金会资助和RAS数学分支计划4的支持。2电子邮件：kuliamin@ispras.ru1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.12.002138V.V. Kuliamin/Electronic Notes in Theoretical Computer Science 111（2005）137软件工程已经发展了各种基于抽象和各种组合的技术来构造复杂的软件系统。它们有助于使软件构造所需的电子邮件的增长更易于管理。不幸的是，现在我们缺乏类似的软件验证和确认技术因此，我们只能彻底验证或测试比我们可以构建的系统更小和更简单的基于模型的测试是检验极其复杂系统质量的一种有前途的方法它的主要思想是用简单的模型抽象目标系统来构造测试，基于模型的测试方法由于所使用的模型可以用形式化的方式表示，并且可以由计算机处理，因此可以另一方面，模型本身可能代表被测系统的不同方面，例如，需求和设计决策，使它们的整理成为可能，以衡量目标系统的各种质量因素但是基于模型的测试在理论上的优势并不直接导致它在实际应用中的有用性。基于模型的方法能否成功地应用于工业中生产的复杂软件此外，在这样的应用中的单一成功并不意味着所使用的技术可以容易地扩展到各种工业软件。所有这些问题都只能通过实验来解决，并找出在工业实践中取得成功的关键方法的特征。ISP RAS的RedVerst [1]团队提出了UniTesK测试开发技术，作为适用于行业的基于模型的测试方法的示例。我们对其适用性的信心是基于在工业软件验证项目中应用类似技术的10年经验但它也有一个基础，在技术本身的独特功能基于模型的测试方法的工业应用需要测试开发和测试的各个方面的全面UniTesK提供了这样的支持，因为它是在文章的主要部分显示。此外，似乎要获得有价值的形式化模型的实际结果，我们需要结合不同的形式化方法。UniTesK是多范式技术的一个例子，在这种技术中，对软件进行正式处理的不同方法处于共生状态，只有一起使用，它们才能实现所述的目标。本文的后续部分考虑了与软件生命周期的所有阶段上的测试开发和测试相关的各种问题。下一节提供了一些问题的描述，以解决的测试开发技术声称其适用于工业软件。本节还简要描述了这些问题在各种形式框架中的现有解决方案。它的主要结论是，没有一种正式的方法可以给出V.V. Kuliamin/Electronic Notes in Theoretical Computer Science 111（2005）137139我们希望在成功的测试开发技术中拥有的所有功能第三部分介绍了UniTesK方法的主要思想，并展示了不同的形式化技术是如何集成在其中的。最后一部分给出了一些结论，并描述了未来工作的可能方向2基于模型的测试开发测试开发的主要问题。每一种声称其适用于各种工业软件的测试技术都必须处理以下问题。• 正确性检查问题当我们想测试某个东西时，我们通常想检查它是否“正常”工作。对于简单的小系统，我们通常非常清楚什么是“正确的”行为，什么不是。对于复杂系统，不仅很难检查它们的行为是否正确，而且正确的行为本身通常也需要更精确地定义，因为很难同时记住系统行为的所有可能变体。测试应该以某种方式考虑到这个精确的定义。• 测试质量评估问题测试开发的全面方法应包括测量测试结果质量的方法这种方法通常被表示为测试覆盖标准。基于目标软件模型的方法应该包含基于模型的测试覆盖标准的定义，可能是相同的。测试覆盖标准的存在允许所谓的覆盖驱动测试，即以最大化所获得的覆盖的方式构建测试。• 测试序列构造问题对于仅基于输入产生输出的系统，高质量的测试只能使用单独的测试动作来构造。这不是软件系统的情况，其行为取决于它们与环境的交互历史，即先前应用的输入。对于这样一个系统，每个好的测试覆盖标准考虑系统状态，这些状态积累了历史上所有实际需要的信息。为了彻底地测试它们，我们需要构造测试动作序列。当允许的操作集取决于先前操作的结果时，任务变得更加复杂。这种情况对于工业软件来说是相当常见的，应该被打算在那里使用的测试构造方法所包含140V.V. Kuliamin/Electronic Notes in Theoretical Computer Science 111（2005）137• 变化的问题众所周知，软件尤其是工业软件不是静态的实体，它总是在变化的。如果测试技术不处理目标软件和环境中可能发生的变化，并且不包含应对这些变化的特殊技术，那么它就不能被认为是工业应用的重要候选技术在软件构造中，最小化变更的影响的常用方法是抽象。我们将看到同样的方法被广泛使用，并且在测试中也提供了良好的结果。• 测试并发性的问题有效的测试技术应该支持当代软件广泛使用的特性.如果我们考虑在现代工业中积极开发并由现代开发技术支持的最对于序贯系统，解释它们对外界作用的反应是相当简单和直接的从基于模型的测试的角度考虑并发性（这也是分布式系统的主要特征），即使在这个看似简单的领域也会产生问题。当我们试图解决并发系统的测试开发问题时，前面提到的问题变得更加困难。有很多形式化方法可用于并发系统的描述、构造和分析。但作者不知道一些正式的，同时全面考虑并发和分布式系统的测试问题的参考文献。首先，如果我们有这样一个系统的模型，如何以一种显式检查其并发行为的方式激励测试操作？如何解释可观察到的系统响应，以检查它们是否符合给定的模型？在这里，我们面临着不明确的概念，并发的行动和不可能引进一个完整的顺序输入的行动和系统的反应，如果他们被观察到在不同的地方，这是常见的并发和分布式系统。针对并发和分布式系统的大多数测试开发技术在这些模型中，唯一与并发相关的特征是它们的非确定性。我们认为这远远不是合适的解决方案，当我们试图为并发系统开发好的测试时，应该明确地处理并发操作。更微妙的问题是，什么样的模型最清楚地给出了V.V. Kuliamin/Electronic Notes in Theoretical Computer Science 111（2005）137141并从测试的角度对前面的问题给出了实用的答案。当然，这需要大量的案例研究和各种方法的应用比较。但现在研究人员甚至没有考虑过它。在本节下面，我们简要地考虑所述问题的现有解决方案2.1行为正确性检查自动校正检查问题的众所周知的解决方案是测试预言机。测试预言机一般是一个程序，它评估目标系统的工作，并决定它是否正确工作。构造预言机的良好来源是以形式化的方式陈述程序行为需求的形式规范。这些规范通常比Oracle本身更清晰和可重用，并且可以通过计算机处理，因此Oracle开发可以自动化。不同种类的规范产生了不同的神谕构建方法。下面我们简单地介绍一下这些主要的方法。对更详尽的综述和技术细节感兴趣的读者可以参考[2]。• 操作规范。 操作规范以要执行的明确操作序列的形式描述系统行为。所使用的操作应该足够简单，以具有明显和精确的语义。与此同时，这些操作的系统应该足够通用，以便能够表示广泛的系统类别。通常使用一些抽象机器的操作。这种规范的例子是各种自动机：从有限状态机（FSM）到图灵机，通过通信和/或扩展FSM（CFSM、EFSM、CEFSM）、标记转换系统（LTS）、输入/输出状态机（IOSM）和转换系统（IOTS）、状态图、定时自动机、抽象状态机（ASM）等。以及基于由某些虚拟机执行的操作的其他并发相关的形式体系和语言也是该方法的示例。VDM或RSL [3]语言中的规范也可以以操作的方式编写。从操作规范中产生神谕的最明显和最常见的方法是执行它们，获得结果，并将其与目标系统的相应操作的结果进行比较。关于基于ASM规范的测试oracle构造的更多细节可以在[4，5]中找到。复杂系统的运行模型通常是不确定的，142V.V. Kuliamin/Electronic Notes in Theoretical Computer Science 111（2005）137因为它们比相应的系统抽象得多。广泛的不确定性是有效测试构造的严重障碍。在微软研究院的软件工程基础小组的工作中[6]，这个问题是通过推迟计算规范结果直到实现结果可用来解决的。当可能的结果集不是太大时，这种方法解决了问题，但它没有覆盖所有可能的系统。例如，当目标系统求解微分方程组时，通常我们不能充分地评估其有效性或基于求解此类系统的某些其他算法这是因为计算的有限精度使得可能有几个局部• 合同规格。软件契约[7，8]将系统的需求描述为其接口操作的契约。经营合同包括经营合同的前置条件和后置条件。前置条件描述了操作的客户端的义务，当其中一个客户端调用此操作时，它应该保持。后置条件描述了当前置条件成立时，系统响应此操作调用的义务。通常，参数类型和接口操作的结果也有契约。一个数据类型的契约被表述为对该类型对象的组成部分的一些约束。这样的约束被称为数据完整性约束或不变量。合同规范由Z、B、VDM、RSL [3]和Ei规范[9]支持。从合约规范构造预言机的方法很明显：我们可以检查前提条件，然后，如果前提条件成立，调用目标操作并获得其结果，然后检查后置条件。不变量可以作为前置条件和后置条件的一部分进行检查。类似的方法在[10，11，12]中使用。该方法的一个问题是存储系统的前状态，它可以用来检查操作执行后的后置条件。另一个问题是主动系统的描述，它可以在没有任何外部刺激的情况下提供动作，并且可能不会终止。用D.”[10]《礼记》：“礼也，礼也。• 公理化规范。公理化规范将系统描述为一组具有相关行为的函数。这些相互关系被描述为对几个功能的组合行为的一组约束。这些约束可以用一阶逻辑或高阶理论来表述。在第一种情况下，这样的规范通常称为代数的。用于代数规范的语言的例子有OBJ、Larch、ML等。V.V. Kuliamin/Electronic Notes in Theoretical Computer Science 111（2005）137143吧严格地说，其他类型的规范可以被认为是特殊类型的axioms。例如，契约也是这样的公理：“当前置条件在操作调用之前成立时，则后置条件在调用之后成立”。但是，合同的结构和处理合同的技术是如此特殊，它们值得单独考虑。作者不知道在测试开发中使用公理化规范，而不是代数规范（例如，高阶理论）。代数规范可以转化为测试，但通常它们几乎不能用来检查系统操作的任意可能调用。在[13]中给出了一个从代数公理构造一般神谕的方法的例子。该方法基于将项改写为规范形，要求代数公理集完备且连续，即保证项的规范形的唯一代数规范的主要问题是它们在现实生活系统中的构造极其困难。规格开发人员应具有先进的数学教育和专业经验，以有效的方式处理这些问题。• 基于历史的规范。基于历史的规范定义了与目标系统相关的一组可能的动作序列。这可以通过对这样的序列的一些约束的帮助或通过显式地表示这样的序列的部分以及针对它们的一些组合规则来完成。基于历史的规范包括使用各种时间逻辑形式主义的方法，这使得可以引用过去或未来，跟踪规范方法和基于时间的方法，包括基于MSC符号的方法基于时态逻辑的Oracle构造方法的例子在作品[14，15，16]中给出。 痕量特异性方法见[17，18]。 在[19]中讨论了基于规范的测试构造。由这类规范构造的预言机通常会评估一些表示与目标系统相关的可观察行为历史的轨迹。通常，没有办法生成一个oracle来评估系统对单个调用的响应行为一方面，基于历史的方法对于提供历史依赖行为的描述是有用的，而不引入用于存储历史信息的辅助变量，但另一方面，它们似乎只适合于一类系统，其行为以特定的简单方式依赖于历史，或者可以通过少量场景的组合来构造。在更复杂的情况下，这些方法变得144V.V. Kuliamin/Electronic Notes in Theoretical Computer Science 111（2005）137−太难用了。2.2测试质量措施为了充分衡量测试质量，应考虑源代码覆盖率和需求覆盖率由于我们在这里考虑基于模型的方法，因此跳过了基于实现的覆盖度量感兴趣的读者可以参考[20]中介绍的基本指标或[21]中的一般调查。基于模型的测试覆盖率标准应与用于构建模型的方法结合考虑• 操作规范。 在操作规范的基础上，将其视为抽象机器的程序，并将其视为源代码来构造覆盖度量，就可以得到测试覆盖度量。在[22]中考虑了基于目标系统的EFSM类模型的覆盖标准。它们分为基于控制流的覆盖，如传输覆盖、传输对覆盖和基于数据流的覆盖，如全用覆盖或杜径覆盖。[23]中给出了基于ASM规范的此类方法的示例基于操作规范的覆盖标准的问题在于它们可能依赖于所选择的建模算法的结构。一般来说，不能保证系统中实际使用的算法具有相似的结构。例如，我们可以计算平方根函数借助迭代过程xn=（xn−1+x/xn−1）/2，作为无限行展开的和（1 +（x1））1/2，或使用恒等式，如如sqrt（x）= exp（ln（x）/2）。这些方法中的每一个都给出了自己的覆盖标准，彼此弱相关。要决定哪一个是最自然的并不容易。我们需要一些特定于实现的信息来选择其中一个更合适的。• 合同规格。如果我们在操作后置条件中分离用不同表达式描述的不同类型的行为，或者尝试将通常的代码覆盖度量应用于被视为代码的前置条件和后置条件，则软件合同可以用于定义类别划分方法[24]是大多数使用合同规范定义测试覆盖标准的方法的起源。这种方法的例子在[25，26]中给出。基于合同规范构建的覆盖率标准可能过于抽象，缺乏对测试质量度量有实际意义的细节。因此，在实践中，它们通常需要用与所考虑的问题相关的额外谓词来扩充。V.V. Kuliamin/Electronic Notes in Theoretical Computer Science 111（2005）137145• 公理化规范。公理化的规范本身提供了基于所覆盖的规则和状态的覆盖标准，它可以被构造为所有可能历史的约简。这些指标似乎过于粗糙，无法发挥实际作用。为了获得更有用的测试质量指标，还需要使用一些额外的技术。例如，我们可以构造一个派生的自动机模型或使用一些组合方法。详情请参阅列表中的最后一项• 基于历史的规范。基于历史的规范只给了我们一组可能的跟踪，我们只能根据实际执行的跟踪来测量测试覆盖率。这甚至比我们从公理中提取的还要少。同样，我们需要添加一些组合考虑，以实现有用的测试充分性标准。参见最后一项关于组合方法的内容。• 概率模型。 概率使用模型给出了一组测试质量度量，评估的不是测试过程中系统特性的探索程度，而是可能使用场景的探索程度。这样的模型可以用来估计被测系统的可靠性。它们通常表示为马尔可夫链，描述外部事件的概率取决于以前的系统-环境相互作用的历史概率模型主要用于指导测试数据的选择。他们提出，例如，在工程[27，28，29]。• 组合方法。 如果我们有一个程序模型，我们通常可以在其中找到各种类型的素元素，这些素元素构成了所有同类的模型。例如，系统的代数描述由许多公理组成，每个公理都是两个操作调用序列的等价我们可以在这里看到的元素-操作的调用，它们的序列，以及这些序列之间的对应关系。类似FSM的模型由状态和转换组成。我们可以引入测试质量的度量，其基于与所执行的测试相对应的素元素的可能组合在代数规范的情况下，我们可以考虑用于测试构造的基础项的复杂性，并通过所使用的项的复杂性来衡量测试的充分性。为了使这个度量更适合实际的测试质量，我们可以引入一个额外的正则性假设，说明只覆盖复杂度小于某个固定值的项是足够的[30，31]。同样的方法也可以用来测量测试质量 基于历史的规范。我们可以尝试计算执行的跟踪的有界长度连续性相对于具有相同长度边界的可能连续性总数的百分比。我们称这种方法为组合方法。 他们可以帮助引进cov-146V.V. Kuliamin/Electronic Notes in Theoretical Computer Science 111（2005）137与使用的任何种类的规格相关的平均标准。它们对于测试充分性度量的实际有用性仍然需要研究。2.3测试序列构造方法基于模型的测试序列构造的方法在这里被认为是与所使用的模型的种类。在大多数情况下，它们的目标是根据一些测试覆盖标准获得高或完全的覆盖。• 操作规范。各种自动机形式的操作规范是最广泛使用的测试序列规范源。在[32，33，34]中给出了基于FSM的测试序列构造方法的系统探索。[35]对基于EFSM的方法进行了回顾。 所有这些方法的主要思想是在状态转移图上构造一组路径，以根据某种覆盖准则获得最大覆盖--覆盖所有转移、所有相邻转移对、所有简单du-路径等。大多数基于（C）（E）FSM模型的方法都提供了测试序列的配置，能够保证模型与成功测试的实现之间的一致性。这些方法及其衍生物用于在SDL[36]、Estelle [37，38]、LOTOS [39]或Statecharts [40]中编写的正式规范的基础上构建测试。在[4，41]中考虑了基于目标系统的ASM规范的测试序列构造方法。这里提出的方法是基于构造一个FSM，其状态对应于ASM规范分支条件中的素逻辑公式有限状态机提供了最合适的和深入研究的测试序列构造方法。它们的主要问题是状态爆炸--当考虑一个实际系统时，它的FSM模型足以进行充分的测试，显得庞大而难以管理。EFSM和其他类型的状态机，可以扩展状态的数据和参数的转换，更适合表示复杂的系统，但不方便分析和测试序列生成。它们以更隐式的方式提供关于系统可能行为的信息，并且需要进行深入的分析，有时不能自动进行，以解释将其以准备用于测试序列生成的形式进行• 合同规格。软件合同本身不能用来构造测试序列。它们应在其他模式中加以改造或扩充，以便对这一目的有用。例如，Dick和Feivre [42]描述了构造FSMV.V. Kuliamin/Electronic Notes in Theoretical Computer Science 111（2005）137147根据合同规范和测试中每个操作的域划分建立模型。定义某些操作的划分元素的谓词在参数-状态空间中考虑。每个谓词对应于一组对（参数，状态）。结果FSM的状态作为这些集合的投影而获得。该FSM的激励对应于所有操作的初始分区的元素。因此，每个操作都会产生几个刺激。这个FSM上的转换之旅提供了所选分区的完整覆盖。类似的技术在[43，44，45]中使用。• 公理化规范。公理化规范很少用于测试序列生成。存在将它们转换为某种自动机的方法。使用公理本身来构造测试序列的一种可能的方法可以基于项重写。我们可以选择一个足够长的种子序列，并尝试以尽可能多的方式重写它，因为它足以满足我们的测试需求，或者由于我们的资源和预算，然后检查初始序列和通过重写获得的任何序列• 基于历史的规范。基于历史的规范给出了基于所描述的可能历史的测试序列构造的明显方法。通常这种规格被转换成一些自动化，以提供更方便的测试序列构造方法。使用基于历史的规范（时序逻辑和MSC）的测试序列构造方法的示例在[46，47，48]中给出• 其他方法。 测试序列构造的其他方法包括概率方法和组合方法。它们通常被设计为最大化一些测试充分性度量。这些指标在前面的小节中讨论过。2.4测试开发中的变更问题通常用于解决软件需求、开发技术、开发团队或系统环境的不断变化所引起的问题的方法是抽象。抽象的描述和规范更易于重用。逐步细化过程有助于生成更详细和具体的规范和代码。抽象和细化也用于应对测试开发中的变化抽象的第一个和最明显的地方是模型和实现之间的边界。如果用于测试开发的模型与实现具有相同的抽象级别和相同的细节，那么它就不能提供有效的测试工具，因为需要增加148V.V. Kuliamin/Electronic Notes in Theoretical Computer Science 111（2005）137发展支出超过两倍。因此，模型通常是实现的抽象。但随之而来的问题是它们之间的一致性关系，这是测试的主要对象学术界的测试开发方法设计者都很重视对所用方法检验的一致性关系进行严格的定义。[33]中给出了基于FSM的方法的此类关系的示例在J. Tretmans[49]的作品中，ioco关系被定义为LTS和基于IOLTS的测试构造方法的为了定义一致性关系，规范和实现被认为是同一类型的模型：两者都是FSM，LTS等。现有定义的另一个特征是可观察事件之间的一一对应输入和输出，具体化和实施。当测试方法应用于实际软件时，这两个因素都可能导致问题。首先，软件需要在方法使用的元模型中隐式地其次，与实现相关的可观察事件通常应该被抽象以保持与模型事件的对应。这样的情况导致用于测试构造的模型和被测试的真实软件之间的抽象级别的转换。这种抽象转换不被方法考虑，通常在所谓的系统适配器中处理，其开发不受任何显式规则的约束有人可能会反对，在正式模型和非正式实现之间开发绑定组件的正式规则不存在。但是应该说明一些规则，以免一旦我们开始开发适配器，形式上定义的一致性关系就与现实不相关我们不仅需要更严格的适配器构造规则，还需要对其可能的功能进行一些扩展。我们认为在使用中引入更复杂的一致性关系是很重要的，例如，将模型视为实现的因子分解[50]。这种复杂性，虽然需要更强的假设进入正式测试的领域，允许更简单的模型和更简单的方法来测试复杂系统的建设，这似乎是相当有用的在实际中。与基于模型的测试相关的变更的另一个重要地方是需求的变更。在这里，系统地使用抽象应该导致各种问题域的系统形式模型的开发。这种模型的开发现在是在OMG的MDA倡议的背景下进行的[51]。这种模型的存在给特定语言的设计者带来了另一个问题-他们应该引入更灵活和强大的重用机制。这种机制应有助于发展更加灵活的V.V. Kuliamin/Electronic Notes in Theoretical Computer Science 111（2005）137149以及基于更抽象模型的可重用测试套件。2.5一般审查结果上述评论表明，系统功能的形式化描述的所有技术都有其优点和缺点。它们中没有一个可以很容易地被认为是最方便用于测试开发的。基于有限状态机的模型对于开发人员来说非常简单和易于理解，可以很容易地用于测试序列生成，但是对于现实生活中复杂的软件来说过于简单。它们可以通过引入数据和转换参数来提高可扩展性，但这样它们就失去了分析的适用性，并且仍然没有获得更隐式描述的通用性和可扩展性，这更适合于构造通用测试预言机。另一方面，代数规范是最隐式的规范，在现实生活的发展中使用起来太困难了。他们也缺乏适当的建设合理的测试充分性度量。解决方案似乎在于整合不同的技术，以便在更适合的领域中使用它们中的任何一种。我们已经提到了使用基于合同规范构建的FSM模型，或者引入组合考虑来基于代数规范度量测试充分性。下一节将详细介绍UniTesK技术，作为测试开发集成方法的一个示例。3UniTesK作为共生解决方案UniTesK [45，52，53]测试开发技术由ISP RAS的RedVesrt [1]小组设计，用于复杂软件系统的工业测试它基于该小组在几个工业软件测试项目中获得的经验，包括电信交换机操作系统、协议实现、P2P消息管理系统以及C和FORTRAN语言编译器。该技术采用基于目标软件形式化模型的测试构造方法。但是为了使这个过程更有效，不同类型的模型被用于不同的发展阶段。该技术包括在其他模型的基础上构建一个模型的方法，从而在测试开发过程中无缝集成它们。 该技术的主要特征、底层测试开发过程和测试架构在文章[45，52]中进行了描述本节将详细介绍150V.V. Kuliamin/Electronic Notes in Theoretical Computer Science 111（2005）137∈∈TFΛ;sUniTesK测试开发中使用的模型，它们之间的关系，以及选择所提出的解决方案的原因。系统行为的功能需求以合同规范的形式表示。合同被选为可以根据建模目标进行抽象或具体化的规范。因此，他们不会在不需要的地方强加太多的决定论，并且在必要的细节上也不会模棱两可。它们结构良好，足够接近需求，因此在实际情况下不会导致大量的开发支出。此外，它们非常适合自动转换为测试预言机。在接下来的章节中，我们将对UniTesK中使用的合同规范中与语言无关的部分进行正式定义然后，我们形式化地定义了合约规范与表示为类型化ASM的目标系统之间的一致性关系由于这种关系在实际意义上的情况下需要太多的工作来检查，我们引入了一个假设，在某些情况下，目标系统的行为等效。良好的候选人，这样的situations是由自然分区的操作域的行为描述的一个相同的约束表达式在postcondition的子域然后，我们给出了一种方法来构建一个自动机模型的基础上给定的规格和一组谓词描述子域的等价行为。当行为等价性假设成立且目标系统服从某些合理的约束时，在该自动机上构造的作为过渡之旅的测试是穷举的，即它们的成功执行证明了规范与系统之间的期望一致性。3.1类型化合同规范一个多排序签名S =（S，F）由一个排序集合S和一个排序集合函数符号F = wS，s SFw;s由函数profiles（w ; s）分层，函数profiles（w; s）由一系列参数排序w ∈ S和结果排序s ∈ S组成。我们经常假设S包含sort bool，F包含bool e和sortt，f∈FΛ;bool，函数<$∈Fbool;bool和函数numb，f∈ F bool，bool; bool，以及对于任意sort s，方程symbol=s∈Fs，s;bool的对称。然后，我们可以定义排序项和函数项或简单的项在签名S =（S，F）上，以下面的归纳方式。• 排序是排序项，函数符号的轮廓中参数排序的序列是空的是项。S<$T<$ 和<$s∈S F<$;s<$F<$• 对于每个轮廓，我们都有变量vi，这是这个轮廓的项。V.V. Kuliamin/Electronic Notes in Theoretical Computer Science 111（2005）137151ΣΣ布尔∈1Ks11，.，s1 l1;s1sk1，.，sklk;sk1K12121• 如果对排序项进行乘积运算，则得到排序项s1×s2s1和s2。Σs1，s2∈Ts1 ×s2 ∈T• 如果我们将一个函数符号应用于一个具有相应轮廓的项数组，我们就得到了一个项。f∈F（s，. . ，s）;s，t1∈F<$，...，t k∈ F<$Σs11，.，s1 lk，.，sk1，.，sklk; s• 如果我们取一对项或一项的投影与相应的轮廓，Σ Σ Σt1 ∈ Fs11，.，s1 k; s1，t2 ∈ Fs21，.，s2 l; s2（t1，t2）∈Fs11，.，s1 k，s21，.，s2 l;s1×s2Σ Σ Σt ∈ Fs11，...，s1 k; s1×s2 π1t∈ Fs11，.，s1 k; s1和π2t∈ Fs11，...，s1 k; s2• 我们得到一个排序项，如果我们根据一个具有profile（s; bool）的项t对排序项s取一个子排序。Σ Σn∈T，t∈F {s：t}∈ T一个多排序结构或简单的结构A的签名S =（S，F）映射每个排序s到一个职业集s A和每个功能符号f∈F s，.，s;s到A的准函数：|一|公司简 介 . ×|一|s→stec|一|S. 如果S包括布尔表达式，KboolA具有精确的两个元素，并将布尔函数的符号映射到这些元素上的相应操作中。方程中的每一个排序符号都应在函数映射中映射相等的元素，将排序的 职 业 设 置 成 t 个 符 号 的 图 像 。Modelmappingg·Acanb eee eextendedontontorttosanddclosedtos（hav-没有自由变量），以一种明显的方式。（s1×s2）A=sA×sAs：tA={x∈sA：t（x）=t}（f（t1，.，t k））A：x<$→fA（t A（x），.，t A（x））1K（t1，t2）A：x<$→（tA（x），tA（x））（πi t）A：x<$→πi（tA（x））签名上的n-公式Φ n是使用量化和逻辑连接从原子公式构建的通常的多排序一阶公式。这些数学形式是函数的一种应用用适当的术语来辩论。f（t， . . ，t）∈F1k152V.V. Kuliamin/Electronic Notes in Theoretical Computer Science 111（2005）137∈闭项的值，一个参数数组上的项的定义，满足A|通过对结构的归纳，定义了结构A中闭公式φ的φ = φ. 适用于Fw;boltoa s序列的参数在A i中成立，所有参数项的值都被定义， f A由这些值定义，等于tA。类型化异步合约规范由以下部分组成• 由一组基本排序和基本函数符号组成的一种基本签名<$b=（• 一种动态签名，包括动态排序集合Sd和动态函数符号集合Fd动态函数符号可能具有混合的配置文件，包括S d的排序和Sort b上的排序项。动态排序和函数-操作符号表示指定系统的状态。此外，我们将联合签名b d =（S b<$S d，Fb<$F d）表示为。• 初始状态规范I，它是一组结构。• 一个过程符号集<$=w∈（Tn）n，s∈T（s∈T一Λ;s 包括─一组过程符号的组合，可以有profiles（w;s）（过程返回值）或（w）（不返回任何内容的过程）。来自ESTA的过程符号旨在指定系统的异步反应• 所有过程的前置条件和后置条件。pre：φ →Φ φ和pre（p）只有自由变量对应于p ∈ φ的自变量。post：φ→ΦφJ，其中φJ被构造得较低。post（p）具有对应于p及其结果的自变量的所有自由Sort of SortJ包含所有来自Sb的基本排序和来自Sb的每个动态排序的两个副本（比如s和SJ）。 函数符号f J包括所有基本函数符号，所有动态函数符号，对于每个动态函数符号f，它们还包括一个函数符号f J，其中f的轮廓中满足的每个动态排序s都被sJ替换。fj的基本排序与f的基本排序相同。因此，我们可以在后置条件中表达对过程调用之前的状态和结果的约束。状态问题是在前状态和后状态中匹配动态排序的相应元素。这个问题可以通过添加跟踪图符号tm来解决（参见[54]以获得更详细的解释和参考）：对于每个动态排序s，s→sJ到n J。此地图旨在绘制一个元素返回到后状态中的同一元素（如果它保留在s中），或者返回到空（如果过程调用将它从s中删除）。我们可以在两个双结构A和Aj中解释公式，以下方式。 基本排序和函数符号被解释为Π∆V.V. Kuliamin/Electronic Notes in Theoretical Computer Science 111（2005）137153S往常未引发的动态排序和符号在A中解释，而它们的引发对应物在A J中解释。符号tms被解释为部分一对一映射tmA，AJ：s A→（sJ）AJ。然后，通过通常的归纳，我们定义满意度（A，AJ）|=闭公式φ∈ Φ <$j的Φ 对（A，AJ）。如果在前面的定义中，difa是空的，我们就说类型化的合约规范。3.2联系方式对于一个表示为类型化ASM的系统（例如[55]关于ASM的一般定义和[56]关于类型化ASM），它具有一个扩展的签名，我们可以定义一致性关系，它形式化了规范和系统之间的一致性概念。首先，考虑没有异步反应的规范。我们需要将过程调用解释为ASM中的转换。要做到这一点，我们应该在ASM排序中添加RISK。 然后，例如，我们可以在ASM签名中使用外部函数符号，在每个状态下，它表示刚刚调用了(it没有参数，并返回一个序列，该序列以来自sort的过程符号开始，以参数sort的值序列结束），以及一个sym- bol out，该sym- bolout具有sort的参数，并返回在当前状态之前调用的过程的结果sort的值。具有静态签名Jbb和动态签名Jdd{in，out}的类型化ASMA符合具有基本签名b的规范，动态签名d、过程集d和可能的初始状态I，i满足以下要求• 对于A的每个初始状态，当我们忽略A签名中的所有附加符号时，它同构于I的某个元素。• 对于A的每个可实现的转换A ›→ AJ（即两个状态之间的转换，其中第一个可以通过A从A的某个初始状态转换来实现），使得在AJ中|= in = p（v1，.，v k）和AJ|= out（p）= r，下面的含义保持A| = pre（p）（v1，.，v k）<$（A，AJ）|= post（p）（v1， . . ，vk，r）。 这就意味着，这种过渡是通过具体化来实现的。在允许异步反应的情况下，一致性的概念它基于UniTesK方法引入的新颖性-普通并发公理。如果一个系统遵守这一公理，那么它的异步反应就可以按照这样一种方式排序，即可以在具体化中找到相应的跃迁序列。为了对这种行为建模，我们需要在ASM中引入额外的函数符号outa，它返回一个元素。154V.V. Kuliamin/Electronic Notes in Theoretical Computer Science 111（2005）137⇒∧∈|然后，系统符合规范，如果在其状态中的可实现路径从初始状态开始并通过调用过程控制，即，在此路径的每一步之后，out返回p∈n或outa返回p∈εa）可以被分割成多个部分，每个部分具有以下性质• 在这一段上调用的过程序列（由out和outA返回的符号可以以这样一种方式排序，即指定状态（结构）之间的相应转换序列是指定所允许的。• 相应的指定路径开始和结束于稳态A1，A2，对于每个pA i= pre（p）. 而作品本身的末端 也是静止的，也就是说，没有从它们到另一个状态的转变，其中定义了a。现在我们已经讨论了系统功能性和一致性关系的规范形式。在一般情况下，实际上对于几乎任何真实（真正用于某些目的）软件系统的例子，我们都可以以描述的方式开发规范，但是不可能构建测试套件来保证在成功执行后系统符合规范。问题在于真实系统的复杂性及其规范的复杂性，即使我们只指定我们真正想要检查的约束。为了应对这种复杂性，我们需要使用其他模型。但是，构建的合同规范应该与该模型有明确的关系为了构建更合适的模型，我们需要引入一些行为等价假设，这有助于将测试所需的样本量减少到可管理的规模。如果我们考虑过程的后置条件，它们可以表示为n正规形式post（p）=i（φi当所有的mulaeφi不依赖于后状态时，即不包括带撇号的符号和对应的变量，到手术结果。这给了我们一个由其前提条件定义的过程域的划分。这个分区的每一部分都被称为一个功能分支。这样的划分是测量测试期间获得的覆盖率的自然工具。我们还可以考虑pre（p）φ i的DNF中单个析取项对应的更