33理论计算机科学电子学札记66（2002）网址：htpp：www.elsevier.nl/locate/encts/volume66.html16页UML模型的验证和自动测试生成：AGATHA方法David Lugato-Céline Bigot-Yannick ValotCEA/LIST/DTSI/SLACEA Saclay -蝙蝠。45191191 Gif sur YvetteCedex{david.lugato，celine.bigot，yannick.valot}@ cea.fr摘要测试生成的相关经济性目标对软件产业来说是非常重要的。寻求提高生产率的制造商需要在系统规范时避免故障：越晚检测到故障，成本就越高。因此，开发能够有效支持负责制定规范的工程师的技术和工具构成了一项重大挑战，其后果不仅涉及关键应用领域，而且还涉及所有那些概念不佳可能对产品品牌形象造成极大损害的领域。本文描述了一组工具的设计和实现，这些工具允许软件开发人员验证UML（统一建模语言）规范。这个工具集属于AGATHA环境，它是一个自动化测试生成器，由CEA/LIST开发。AGATHA工具集设计用于验证使用EIOLTS形式主义（扩展输入输出标记转换系统）描述的通信并发单元的规范。本文所描述的工作的目标是提供一个UML和EIOLTS形式主义之间的接口，使使用AGATHA的UML规范的可能性。在本文中，我们首先描述了UML模型的翻译到EIOLTS形式主义，并翻译的行为分析的结果，提供AGATHA，回到UML。然后，我们提出了AGATHA工具集，我们特别关注AGATHA如何克服组合爆炸的几个问题。我们揭示了符号演算和冗余路径检测的概念，这是AGATHA的内核的主要原则。该内核正确地计算EIOLTS中指定的系统的所有符号行为，并通过约束求解的方式自动生成测试。最后，我们将我们的方法应用到一个例子中，并解释计算的不同结果。关键词：UML规范，自动测试生成，符号演算。© 2002由Elsevier Science B.V.出版。在CC BY-NC-ND许可下开放访问。LUGATO，BIGOT，341 介绍形式化方法允许系统分析和测试生成规范。这提供了对系统行为的早期反馈。该规范分析步骤的经济目标是相当可观的，因为它同时降低了验证的成本和时间，同时增加了系统的可靠性。但是这些形式化的技术通常是相当复杂的：这就是为什么这些技术在这个时候还没有渗透到工业领域的原因。因此，至关重要的是提供工具，使这些技术自动化。众所周知，分析系统的难度取决于规范的“质量”。这就是为什么在指定系统时遵守一些规则是至关重要的。因为一般的UML模型仍然有很多变量、开放或未定义语义的点[1]，形式化分析需要尊重建模规则和一些UML专门化。这些专业化是附加或专用于欧洲项目AIT-WOODDES [2]。已经开发了一些方法和工具来使用系统规范分析系统（以防止意外行为）和生成测试（以保证实现对模型的适应性）。AGATHA等工具生成测试集，允许验证软件实现是否符合其规范（黑盒测试）。由于它还生成一个符号执行树，AGATHA允许深入调查系统的行为。为了产生这些结果，AGATHA必须处理组合爆炸。我们将在本文的第二部分看到AGATHA如何克服这个问题。AGATHA工具集是不同技术的熔炉，如[3]所示。内核是基于符号演算，检测交错，约束求解，重写程序，多面体演算…像[4]一样，AGATHA工具集为UML状态图生成一组测试，但是它不需要测试需求来计算详尽的符号路径覆盖。注意，Hartmann的工具和这里介绍的工具中使用的UML语义也有一些不同之处我们工作的第一步是开发UML和AGATHA使用的A-EIOLTS（AGATHA扩展输入输出标记转换系统）语言之间的接口，特别注意尊重每种语言的语义特性。我们在Objecteering UML建模工具中实现了最终的翻译算法[5]。规范的形式验证以及软件测试通常需要高技能、时间和人员。在本文中，我们讨论了添加到AGATHA的新功能，以便以透明的方式使用它，并详尽地计算规范的行为。我们希望促进一种渐进的方式来详细说明规范。正如将要演示的那样，该工具集帮助工程师在任何步骤中正式验证所开发的系统。我们希望坚持使用AGATHA来验证UML规范的透明性。由于AGATHA技术的完全自动化，开发人员将能够在使用UML CASE工具进行建模的同时验证规范，然后还可以为实现生成测试。2 将UML模型转换为A-EIOLTS我们将AGATHA工具集连接到AIT-WOODDES项目的环境中，该项目提供了一种设计UML规范，自动代码生成器和验证工具的方法。在这种情况下，我们生成测试的UML模型设计与ACCORD方法[6]。公认的UML模型都是用类图设计的。每个类都应该有一个或多个状态图来表示它的动态行为。协作图用于对类实例之间的交互进行建模。AGATHA提供的结果将转化为UML序列图。LUGATO，BIGOT，35相互作用U M L E D itor（Objecteering）2.1 两步法转录从UML到A-EIOLTS的转换是一个两步过程。首先，根据一致性规则检查UML规范，以验证转换模块将能够将规范转换为A-EIOLTS;该模块还将UML模型转换为另一个UML模型，具有等效的语义，但仅使用一组受限的UML元素。然后第二个模块将这个受限的UML转换成一个A-EIOLTS文件。在下面的部分中，我们只描述第二步翻译器。另一个模块可以分析结果文件，并将结果带回Objecteering CASE工具，例如，动画状态图显示给定测试用例中涉及的对象的状态机的执行（参见图1）。所使用的UML子集被设计为在状态机的描述中实现与AGATHA的A-EIOLTS输入语言相同的简单性水平。第二步是将“简化的UML”转换在这个项目中，类图用于表示所涉及的类，协作图显示这些类的不同实例交换的消息，对于每个类，状态机及其状态图显示对象的行为。序列图可用作反馈，以表示AGATHA提供的不同可能测试。用户2.2 活动对象图1UML定义了一种称为活动对象的对象类别。每个活动对象都有自己的处理资源（通常，它们有自己的任务、进程或线程）。因此，活动对象可以与其他对象并发运行。它们与被动对象相反，被动对象有自己的数据，但只有在主动对象调用时才执行，主动对象将其线程借给被动对象以执行请求的操作。当活动对象与UML状态机相关联时，它有一个事件队列，允许它们存储传入的事件，直到状态机能够处理它们。在此项目中，转换后的模型必须仅包含活动对象。2.3 AGATHA我们在这里只描述A-EIOLTS的一般原理。这种形式主义的灵感来自于ESTELLE语言的简化版本[7]。反式从状态1到状态2当输入（x）提供x > 0输出ok开始a：= a + x;END;图2-发展工具开发工具UML A-EIO LT SMod el S percificationUMLFE EDBACK（E xh austive路径）结果结果分析表明，T w o -步骤规范内拉托尔山AG ATH AState1？input[ x > 0]！a：= a + x;状态2LUGATO，BIGOT，36分层模块结构被限制为仅在最低层具有通信控制器的平面结构。每个模块都由I/O消息和变量的声明、自动机的节点列表以及这些节点之间的转换列表组成（参见图2 A-EIOLTS转换的示例）。以下限制也适用：模块之间的通信仅限于同步会合，不允许多个集合：一个集合必须只包含两个自动机（或模块，发送者和接收者;既不支持多个接收者，也不支持消息的广播）。当消息的接收者是一个模块时，OUTPUT指令会锁定其模块，直到发生会合（如果有的话）。另一方面，发送到环境或从环境接收的消息被认为是异步发送的，因此是非阻塞的。由于会合必须只包含两个模块，因此在给定时间，一个模块只能向另一个模块发送一条消息。由于输出是锁定的，因此不再可能遵循扩展转换系统的语义。在扩展的转换系统中，您可以在转换的操作中发送消息，这些操作不再限于分配。为了重现这种语义，有必要创建中间状态。因此，融合的控制器变得静态可计算，会合不再依赖于行动。变量管理是在转换的主体中执行的，使用0级PASCAL指令。可以在转换上指定的操作仅限于以下集合：变量，例如X，Y，功能：+|-|或|和|...（操作员）0|1|...|真|（常量）表达式：X：=E（赋值）C; C '。（排序）如果E则C;否则然而，重要的是要注意，该子集允许用户表达任何复杂的指令。保护（'PROVIDED'）是逻辑类型的，但是注意，为了验证SDL规范，已经添加了临时保护[8]。必须尽可能避免全局变量，因为组合爆炸的风险特别重要。请注意，从行为的角度来看，使用全局变量是没有根据的。2.4定义受限UML状态机我们定义了一个受限的UML状态机（或简化的UML），它是对与状态机相关的UML概念集的限制。任何状态机都可以转换成这个子集，而不需要修改语义。为了容易地翻译成A-EIOLTS，受限UML必须具有类似的复杂性。因此，仅支持简单的状态和简单的转换。UML状态机的事件处理机制链接到UML对象，并且不能更改。因此，就像简单的状态和转换一样，事件处理机制是UML语义的基本元素，并保留在受限UML的语义中。在UML规范中，调用事件表示接收到同步调用特定操作的请求。A-EIOLTS只支持每个转换一个调用事件。要在转换上执行的操作只能由一个类型为CallEvent的操作组成它将LUGATO，BIGOT，37源状态目标状态已经有可能向环境添加操作调用，但是我们通过每个转换只允许一个操作调用来保持简单，从而抑制了区分操作调用接收者的需要。请注意，调用自己的操作之一的对象被视为CallEvent。根据A-EIOLTS的限制，输出不可能是A-EIOLTS转换操作的一部分。一个直接的后果是CallEvent不能是UML转换操作中的条件表达式的结果。此外，AGATHA总是先发送OUTPUT消息，然后再执行动作。这可以防止在发生多个操作后发送消息（特别是，消息的参数将不依赖于这些转换中的操作）。简而言之，受限的UML只允许一个CallEvent或者（不包括）一系列的赋值（见图3中接受的转换的说明）。Event（params）[Guard] /Actions图3最后，受限UML由以下规则定义：仅支持简单状态（不支持复合状态），只接受简单的转换（除了初始伪状态之外没有伪状态），仅在转换时接受操作（状态上无活动、无进入和退出操作），在条件测试（IF-THEN-ELSE）中无呼叫操作，转换上的操作可以是单个CallAction，也可以是（排他地）一系列赋值和条件测试，由分隔符（UML活动对象或A-EIOLTS模块以异步方式并发执行。但是对于UML活动对象，通信是异步的，对于A-EIOLTS，发送消息会阻塞源模块，直到消息被目标模块接收（同步会合）。因此，UML事件处理中涉及的机制被精确地转换为A-EIOLTS描述，以获得相同的通信语义。在下一小节中，我们将介绍这种机制的转换，然后介绍执行模型的概念，这与必须执行转换的方式有关。2.5 拆分对象根据UML规范（OMG-UML V1.3，§2.12.4UML仅将此表示作为一个示例，并指出任何其他实现相同语义的机制都将符合规范。但是这个例子非常接近A-EIOLTS所支持的，我们的实现也是如此。这三个要素的定义如下：一个事件队列，它保存传入的事件实例，直到它们被调度;事件调度器机制，其从事件队列中选择事件实例并将其出队以进行处理;一个事件处理器，它根据UML状态机的一般语义和所讨论的状态机的特定形式来处理调度的事件实例;因此，UML规范称之为LUGATO，BIGOT，38因此，我们自然地为每个UML活动对象附加两个A-EIOLTS模块：第一个模块是事件处理器。它的A-EIOLTS规范在全局上类似于相应的状态机，即使关闭视图会显示微小的更改（转换拆分为几个较小的转换，附加状态，添加控制消息等）。事件处理器知道给定活动对象的行为、状态和转换。第二个模块是事件调度器，它在A-EIOLTS的同步会合模型之上实现异步通信。事件调度程序必须随时准备好接收来自任何源的事件，即使事件处理程序由于正在处理另一条消息而尚未准备好处理这些事件。为了存储接收到的事件，事件调度器必须在其模块中实现事件队列。事件调度器不知道状态机的结构;另一方面，它知道事件处理器可能接收到哪些事件，尽管它不知道什么时候可能接收到它们。（YHQW IRU0\2EMHFW8 0/$FWLYH 2E MH FW？0\2E MH FW？$（，2/7602 '8/（FRUUHVSRQGLQJ WR80/？V2019年10 月15 日，中国国际航空航天博览会在北京隆重开 幕。$（，2/76 02 '8/（FR UUH VSR QG LQJ WR80/ ？VHYHQW SURFHVVRUevt我的目标（YHQW IRU0\2EMHFWevtT ran s late d to（YHQW TXHXH）80/VWDWHP DFK LQ HG HVFULE LQJ WKHDF WLYHR E MHFW？VE HK DYLRU(YHQW WDNHQ RXW RI WKHTXHXHIRUSURFH VV LQJ（YHQW WDNHQ RXW RI WKHTXHXH IR U SURFHVVLQJ$（ ，2/76VWDWHFKDUWUH SUHVH Q WLQJ WKH EHKD Y LR URI80/？VDFWLYH RE MHFW图4 -已经实现的第一执行模型包括先进先出队列（参见图4以获得该分解的概述）。这种分解对应于UML标准提出的结构。事件调度器接收所有事件。如果事件处理器忙，则调度程序存储事件以供以后处理;否则，事件将直接传输到处理器。因此，事件分派器充当活动对象的输入接口。另一方面，输出由事件处理器直接发送到其他活动对象。在事件处理器必须向自身发送事件的情况下，它实际上会将事件发送给它的调度程序，就好像它是另一个活动对象一样。2.6 执行模型UML的限制强加了事件处理的草图，但是许多细节留给了实现者的判断。由于我们的目标是分析系统的精确行为，因此我们必须强加执行模型的精确细节。在这样的执行模型中描述的细节包括但不限于事件的处理。如果将事件分派器视为黑盒，它将获得模块性。我们尽可能地坚持这种观点，尽管我们最初为调度器使用FIFO列表。“The processing of a single event by a state machine is known as a 在开始运行到完成步骤之前，状态机处于所有动作（但不一定是活动）都已完成的稳定状态配置中。相同的条件如果为OMyO对象LUGATO，BIGOT，39在运行至完成步骤完成后应用。因此，当状态机处于某种中间和不一致的情况时，事件将永远不会被处理。运行到完成集是状态机的两个状态配置之间的通道。（OMG-UML V1.3，§2.12.4.7）这意味着活动对象一次只处理一个事件。不过，它可以在这段时间内接收其他事件，并将其存储起来供以后处理。当事件处理器正在处理一个事件时，它不能处理另一个事件：事件调度器将对任何传入的事件进行排队。所有以处理器为目标的传入事件都将首先通过事件调度器，因此处理器将永远不会从其调度器之外的其他对象接收传入事件。因此，调度程序可以肯定地知道处理器何时进入RTC步骤，因为它刚刚发送了相应的事件。现在，如果我们为事件处理器提供一种方法来告诉调度器它离开RTC步骤，那么调度器将可靠地知道处理器何时繁忙以及何时准备就绪（空闲并准备好接收事件）。从这个模型中，我们可以为事件调度器定义一个通用的状态机。图5所示的调度器使用一个变量来存储从一个转换到另一个转换的消息类型。包含意外和/或错误行为的规范可能导致事件分派器的洪泛。这样的泛洪将通过一个测试生成器工具集几乎无限地探索。出于这个原因，我们通过限制FIFO的大小来增加另一个保护措施。当调度器的FIFO已满时，调度器将死锁。这样，执行路径将被通知为错误。（PSW“0VJ3URFHVVHG>HPSW\TXHXH@“0HVVDJH0HVVDJH“0VJ3URFHVVHG公司简介企业文化荣誉资质企业文化“0HVVDJH0HVVDJH公司简介>PVJ 0HVVDJH @0HVVDJH“0HVVDJH 4XHXH0HVVDJH“0HVVDJH 4XHXH0HVVDJH联系我们>PVJ 0HVVDJH @0HVVDJH图52.7 过渡和可用性在事件处理器中分割转换并不会真正改变执行的语义。事实上，它甚至会增强模拟。例如，考虑对象1向对象3发送两个事件（a，b），并且对象2也向对象3发送一个事件（c）。任务调度的明显随机性可以改变对象3接收事件的确切顺序（c，a，b/a，b，c/a，c，b）。第三种情况，为了被测试生成器模拟，需要在不同的转换上发送a和b（并且这在A-EIOLTS中是强制的，每个转换只有一个Renaissance）。事实上，A-EIOLTS关于发送和接收事件的明显繁琐的限制具有积极的影响，因为执行路径的分叉通常来自事件的这种重新排序。事件调度器对所有的事件处理器都有责任：它必须总是准备好接收事件。但即使是事件调度器也需要一些时间来存储、恢复或发送事件;在此期间，它不可用。关于活动对象之间究竟发生什么类型的通信，还有其他考虑因素。因此，在临界区执行事件排队和分派操作是非常常见的。一LUGATO，BIGOT，407UDQV2号！0HVVDJH0VJ$FN%HIRUH2QH“0HVVDJH0VJ3URF%HIRUH7ZRLVSDWFKHU！0VJ3URFHVVHGLVSDWFKHU！0VJ$FN“0HVVDJHLVSDWFKHU！0VJ3URFHVVHG6WDWH2QH6WDWH7ZRLVSDWFKHU！0VJ$FN“LVSDWFKHU！0VJ3URFHVVHG0VJ3URF%HIRUH2QH“0HVVDJH“0HVVDJH2号！0HVVDJH0VJ$FN%HIRUH2QH7UDQV临界区是一个线程对一组线程中的所有线程具有排他和绝对优先级的区，是一个在结束之前不会被中断的执行区。 在消息的排队和分发的情况下，线程集就是整个系统，并且这样的操作被认为是全局原子的。2.8 通用事件处理程序如前所述，事件处理器不需要能够在任何时候接收消息，调度器负责这方面的工作。另一方面，处理器知道对象处于什么状态，以及它可能接收到什么事件。我们将通过几个步骤构建一个通用事件处理器。作为一个例子，考虑图6中的UML状态图：0HVVDJH 2！0HVVDJH0HVVDJH！0HVVDJH图6现在让我们把它转换成一个简单的A-EIOLTS状态图。第一个问题是调度器不知道处理器准备接收什么，这意味着如果一个意外的消息到达，事件调度器仍然会将其发送给处理器。实际上，调度器将尝试发送一个处理器永远不会接收到的消息，因为它将永远等待调度器发送另一个消息。调度程序知道活动对象没有改变状态可能会很感兴趣。事实上，它对于处理延迟事件很有意思，这将在下面进一步解释。为了区分使状态机改变状态（或者更准确地说，改变状态或执行外部自转换）的消息和不改变状态的消息，事件处理器将在状态改变（或外部自转换）时返回MsgProcessed，或者对于不引起状态改变（内部转换）的消息返回MsgAck。现在我们可以编写新的事件调度器了（见图7）。当调度程序发送意外的消息时，这个线程不会死锁。请注意，应该相应地更改事件调度器以处理新的MsgAck回调，但是，目前，我们不会详细说明它：此时唯一必要的修改是复制所有将MsgProcessed作为触发事件的转换，创建一个具有完全相同子句但在MsgAck上触发的孪生转换。图72.9 延迟事件和参数UML包含了一个A-EIOLTS中没有的概念：延迟事件。对于一个特定的状态，可以指定，尽管在该状态下不能处理特定的事件，但对象必须保留此事件。当状态更改时（或当触发外部自转换时），将再次检查延迟事件。如果在此新状态下无法处理该事件，则将使用延迟事件，而不会产生副作用;如果处理了延迟事件，StateOne国家二LUGATO，BIGOT，41触发相应的转换。如果事件再次被延迟，则再次存储它以供以后使用，依此类推。，QFRPLQJ HYHQWVDUHLQVHUWHGDWWKHEDFN7KH LWHUDWRU QHYHU JRHV SDVW WKHILUVWUHJXODU HYHQW 7KH RWKHU UHJXODUHYHQWVZLOO GURS QDWXUDOO\WR WKLVSRVLWLRQ'HIHUUHG HYHQWVDUHLQVHUWHGKHUH电话：+86 2873877KH LWHUDWRU VWDUWVDW WKH KHDG RI WKHOLVW RQHDFKVWDWHHQWU\图8当处理器在不离开状态的情况下消费延迟或常规事件时，重试队列中不合格的第一个事件是毫无意义的。不仅如此，如果在状态机处于特定状态时添加了新的延迟事件，那么至少在下一个状态更改之前，它将无法触发转换。出于这个原因，我们可以定义一个迭代器来在每次状态改变时，迭代器将被重置为FIFO的头部，符合延迟事件具有优先级的事实。如果迭代器到达第一个常规事件，它将不会继续前进，因为在该插槽中总是有一个事件准备好被发送到处理器，除非所有非延迟事件都已处理。到目前为止，我们一直考虑不带参数的简单事件，但用户可以发送带参数的消息。在FIFO中存储参数很容易。我们不是只推送消息ID，而是推送消息ID及其所有参数。当一个消息必须弹出时，第一个POP操作将检索消息ID。因此，调度程序将知道FIFO中有多少参数，并立即弹出它们。2.10 关于执行该生成器是使用Objecteering的UML Profile Builder开发的。概要文件构建器允许用户通过 使 用 标 准 UML 扩 展 机 制 （ 原 型 、 标 记 值 等 ） 或 使 用 J 语 言 添 加 行 为 来 扩 展Objecteering的功能。J是一种面向对象的编程语言。J语言的主要特性是它能够导航元模型：当前项目的模型在内存中可用，并且可以根据Objecteering的元模型进行导航3 AGATHA内核在介绍了从我们的UML模型到A-EIOLTS的转换之后，我们在本节中描述了AGATHA所基于的主要原则，这些原则使组合爆炸问题处于困境。我们将看到AGATHA如何使用不同的学术技术来计算系统的行为。3.1 AGATHA定位有几种方法可以验证系统规范。第一个是定理证明和模型检验[9]。这类技术已被证明是成功的验证系统的关键部分但这些技术仍然存在两个主要缺点HPSW\(YHQW（YHQW）(YHQW'HIHUUHGHYHQW'HIHUUHGHYHQW'HIHUUHGHYHQW1H[W HYHQW，呼呼LUGATO，BIGOT，42由于可变域的组合爆炸，对于模型检查;以及需要开发人员的高级技能自动测试生成是解决系统验证问题的另一种方法。一致性测试是这个领域中最知名的部分。虽然AGATHA能够为实现生成测试，但对该特性的讨论超出了本文的范围。我们的第一个目的是验证规范本身，并顺便生成测试，以便在规范中模拟它们。大多数验证工具使用枚举技术，因此在尝试彻底识别系统的执行树时受到组合爆炸问题的限制。一些验证工具将验证集中在特定方面：测试目的[10]，时间属性[11]等。我们希望在AGATHA中构建的解决方案是一个详尽的符号路径覆盖。请注意，这个标准将有助于在未来使用AGATHA进行验证。如果我们想证明一个规范上的属性的真实性，由于AGATHA获得的穷举性，我们只需要在获得的路径上证明它。以下小节概述了AGATHA中使用的不同学术技术，以达到这种详尽的路径覆盖。3.2 主要原则：象征性执行AGATHA使用[12]，[13]，[14]定义的“符号执行”。数值技术的主要缺点是由于可变域的组合爆炸。这些领域可以是巨大的，有时甚至是无限的。符号演算允许处理这样的域，因为计算所有的行为并不等同于尝试所有可能的输入值。它们不给输入赋值，而是在整个执行过程中保持符号状态。因此，每个行为不再依赖于完全执行的微积分的结果，而是依赖于表示对由条目符号表示的变量的约束的表达式。从执行点触发的每个转换都会在变量上添加一个新的约束。在执行的任何一点上，整个约束都被称为“路径条件“。首先，简单比较一下符号状态和数值状态：数值状态是由自动机中的状态和变量的数值定义的，而符号状态则是由状态、变量的符号值和路径条件定义的（见图9的简短示例）。考虑图中的过渡。第二章：反式从状态1到状态2当输入（x）提供x > 0输出ok开始a：= a + x;结束语：对于初始状态：数值状态=（s1，0），a0 = 0符号状态=（s1，a0，true），包含（s1，0）对于最终状态：数值状态=（s2，1），x = 1符号状态=（s2，a0 + x，x>0），包括（s2，1）图9一个符号状态可以表示一组无限的数值状态。作为AGATHA演算结果的执行树是符号状态的有限树。因为AGATHA是穷举的，并且力求最小，所以我们希望执行树尽可能短LUGATO，BIGOT，43现在，如果我们想检测尽可能多的冗余路径，我们需要使用归约过程。3.3 减少过程执行树的构造从属于归约过程，以便通过以下策略消除尽可能多的冗余路径：当从布尔标准或多面体标准检测时，切割“空”路径条件。我们使用Presburger工具和定理证明器来实现这一点。避免计算可从另一个模中扣除的路径，交织检测不如[15]中复杂：没有任何时间约束的内部过渡与其他过渡。计算每个符号节点的比较过程并引用已经存在的符号。符号节点的n元组是n个并发模块中每个模块的实际控制节点的列表。这三个归约过程是避免状态爆炸问题所必需的。我们使用几种不同的算法来计算每个符号节点的比较过程：ControlNode过程：如果两个控制节点的n元组相等，则两个符号节点是等效的。包含过程：如果两个符号节点的n元组相等，并且其中一个的变量域包含在另一个中，则两个符号节点是等价的。相等过程：如果两个符号节点的n元组相等，并且它们的变量域相等，则两个符号节点是等价的。但有时引入抽象来降低复杂性也很有用。我们目前正在自动化几个不同的抽象。值得注意的是，在许多规范中，没有人为干预来提取或调整规范并获得结果。使用规范的抽象模型，AGATHA演算总是终止，因此获得的执行图是穷举的。3.4 简化程序执行点越深，表示其路径条件的表达式就越大。变量的符号表达式也可能快速增长。这就是为什么简化过程必须“即时”应用，以缩短表达式并检测无用路径[16]。到目前为止，我们使用基于重写技术的简化器。重写引擎是Brute [17]，Brute是CafeOBJ工具集的一部分。AGATHA的重写规则文件实际上由三百多条规则组成。这些规则允许将符号表达式保持在合理的大小范围内，并获得表达式的范式，从而简化了算法（如比较过程）中所需的表达式之间的比较。我们还使用多面体工具Omega [18]来计算包含和相等过程。使用这个工具，我们能够比较两个符号节点的变量域。3.5 组合物符号执行过程在一个模块上执行，但全局应用程序（历史上AGATHA被设计用于验证并发嵌入式系统）通常由许多模块组成，因此必须将它们合并。有两种可能的方法来合并模块。第一个解决方案是使用Milner [19]介绍的组合物。全局模块由其LUGATO，BIGOT，441111 1movement_order（x：：{up，down，stop}）init_engine（）asked_stage（x：integer）ack（）crossed_stage（x：integer）stopped_cabine（）departure（x：方向：{向上，向下，停止}工程经理current_stage：integer请求楼层：integer初始阶段：integerengine_control（x：integer发动机电梯管理器call（x：integer）reached_stage（）init_stage（）ask_stage：整数11button（x：integer）用户StageRecord/EngineManager_1：EngineManager除了那些由会合同步的分量之外，这些分量由通过消除交换参数而获得的等效跃迁代替。另一种解决方案是首先计算每个模块上的符号执行，然后合并结果以获得全局应用程序行为。后一种方法的主要好处是演算的并行化：每个模块的执行树可以单独计算。目前，只有第一个解决方案在AGATHA中实施。第二个方案将很快纳入。但是已经可以在规范的选定模块的子集上计算执行树。所有的可扩展模块都被认为是环境，来自这些模块的消息可以以所有可能的顺序出现，并带有自由参数。3.6 约束求解器一旦计算出执行树，系统的整个行为就展现出来了。活锁和死锁是可见的。我们使用DaVinci [20]图形界面来表示执行树。然后，约束求解器可以用于获得满足路径条件的符号变量的适当值，并生成数值测试输入序列。AGATHA可以使用两种不同的约束求解器：Presburger工具Omega或Con'Flex [21]。我们选择为每个符号测试生成一个数值测试。每个符号测试代表一个等价类的数值测试，约束求解器只计算一个解决方案的每个路径条件。在UML规范的情况下，这个数字测试的格式是一个序列图。4 示例在本节中，我们将展示一个4.1 电梯我们定义了一个简单的电梯规范。我们定义三个类：一个用于记录用户所要求的阶段，一个用于管理电梯的引擎，一个用于管理电梯以及阶段记录器和引擎管理器之间的交互。我们还定义了代表外部系统的两个参与者：用户和电梯本身。所以我们设计了如图10所示的类图。免费WiFi呼叫按钮1初始阶段到达级询问阶段离港停机舱交叉级ack初始化引擎移动命令/User_1：使用r/Engine_1：引擎发动机控制图10此外，正如我们之前所说的，我们需要一个协作图来突出类和外部系统之间的不同交互（参见图10）。对于每个类，我们构建一个定义行为的状态机（见图11和图12）。/LiftManager_1：LiftManager/StageRecord_1：StageRecordLUGATO，BIGOT，45call/asked_stage：=x;User_1->button（asked_stage）;LiftManager_1->asked_stage（asked_stage）;movement_order[x=stop]movement_order[x>stop]/direction：=x;LiftManager_1->ack（）; Engine_1->engine_control（direction）;_阶段direction：=stop;Init初始发动机关闭movement_order[x=stop]/direction：=x;LiftManager_1->ack（）;发动机1->发动机控制（方向）;对movement_order[x>stop]/direction：=x;LiftManager_1->ack（）;图11-阶段记录器（左）和引擎管理器（右）的状态机问阶段[x=当前阶段]Init出发/StageRecord_1->init_stage（）;EngineManager_1->init_engine（）;initial_stage：=x;current_stage：=initial_stage;asked_floor：=initial_stage;asking_stage[x>当前阶段]/等asked_stage[x当前阶段]/stopped_cabine/StageRecord_1->reached_stage（）;停止EngineManager_1->movement_order（up）;mysql：=x;EngineManager_1->movement_order（down）;asked_floor：=x;ackWait_ack_on等待_ack_stopackOncrossed_stage[x=asked_floor]/current_stage：=asked_floor;EngineManager_1->movement_order（stop）;4.2 运行工具集crossed_stage[x>asked_floor]/current_stage：=asked_floor;图12AGATHA工具集主要有三个步骤：将UML规范转换为A-EIOLTS形式，生成符号测试用例，并将这些符号测试用例转换为UML序列图。4.2.1 翻译UML规范到A-EIOLTS的转换从初始模型的拆分开始。有了这个第一级转换器，组合的转换被分成几个转换。作为阶段记录器的示例，空闲和占用之间的转换被分成具有两个新状态的3个子转换（参见图13）。/asked_stage：=0;Init初始阶段空闲call/asked_stage：=x; reached_stageS1«内部»占据User_1->button（asked_stage）;LiftManager_1->asked_stage（asked_stage）;S2«内部»图13在一个简单的图中扁平化的状态机可以很容易地转换为A-EIOLTS形式主义。这使得某些转换成为原子的，并使规范的分析更加精确。第二个翻译器使用A-EIOLTS形式生成模型。每个类由两个A-EIOLTS模块镜像：一个对应于UML/asked_stage：=0;Init初始阶段空闲达到占据LUGATO，BIGOT，464.2.2 符号测试用例该工具根据A-EIOLTS规范计算符号执行树，该树的每个路径代表一个符号测试用例。在这个例子中，让我们仔细看看符号树的构造（见图14）。对于树的每个符号状态，我 们 以 5 元 组 的 形 式 提 供 变 量 的 值 ： [StageRecord.asked_stage ，LiftManager.current_stage ， LiftManager.asked_floor ， LiftManager.initial_stage ，EngineManager.direction]，并且我们提供所有遇到的守卫的合取（也称为路径条件）。符号执行树从每个状态机的初始状态开始：Init，Init，Init，5元组等于[0，$，stop]，其中$表示不受影响的变量，路径条件（PC）等于TRUE。这个$ value标识了那些没有初始化就被使用的变量。第一个可触发的转换是从提升管理器状态机的Init到Wait。该转换等待来自发动机的外部消息（离开），该消息使升降舵和初始级停止。然后发送事件以初始化阶段记录器（ StageRecord_1->init_stage （ ） ） 和 引 擎 管 理 器 （ EngineManager_1->init_engine（ ） ） 。 5 元 组 等 于 [0 ， departure_1 ， departure_1 ， departure_1 ， stop] ， 其 中departure_1表示消息接收的值，PC保持TRUE。在每一步中，该工具计算所有可触发的转换，以及每种情况下的5元组和PC。对于每次计算，该工具将新的符号状态与已经计算的符号状态进行比较。如果控制节点相同，则比较变量的域。如果存在验证新符号状态的约束但不验证旧符号状态的约束的数值5元组，则计算继续，否则计算停止。例如，在符号状态#9 Occupy，On，On中，5 元 组等 于[call_1 ，departure_1， asked_stage_1 ，departure_1， up]， PC等 于departure_1>asked_stage_1。如果工具选择从提升管理器的打开到打开的转换，则新的符 号 状 态 对 应 于 #10 占 用 ， 打 开 ， 打 开 ， 5 元 组 等 于 [call_1 ， crossed_stage_1 ，asked_stage_1 ， departure_1 ， up] ， PC 等 于 depa
我的内容管理
展开
