面向服务架构下的图转换系统中可靠消息传递的建模与验证

理论计算机科学电子笔记175（2007）37-50www.elsevier.com/locate/entcs图转换系统对可靠的建模和验证4L'aszloGéonczy1、Ma't'eKova'cs2和Da'nielVarro'3布达佩斯技术经济大学测量与信息系统系匈牙利摘要在面向服务的体系结构（SOA）中，由于对高可靠服务的需求不断增加，服务级协议越来越多地包含了诸如安全性、可靠性、可用性等非功能性方面的内容。当一个服务不能提供所需的QoS时，服务请求者需要在交换后动态地切换到一个具有足够服务参数的新服务一系列信息在本文中，我们首先使用服务中可靠消息传递所需的参数扩展核心SOA元模型。然后，我们通过图转换规则对可靠消息传递的重新配置进行建模。最后，我们进行了正式的验证，建议的规则集结合分析工具，图转换和标记的转换系统。关键词：面向服务架构，图转换，可靠消息传递1引言面向服务的体系结构（SOA）为实现业务关键型服务提供了一个灵活的动态平台。SOA范例的主要业务级驱动因素是组件化，它在分布式应用程序的设计过程中提高了从对象到服务的抽象级别。SOA范式的主要架构级驱动因素是提供一个通用的中间件框架，用于独立于实际业务环境的服务组件的动态发现、交互和重新配置。最近，服务的非功能性参数的识别已经通过与Web服务相关的各种基于XML的标准（诸如WS-可靠消息传递、WS-可靠消息传递策略等）来解决。可靠的消息传递-1电子邮件：gonczy@mit.bme.hu2电子邮件：km432@hszk.bme.hu3电子邮件：varro@mit.bme.hu4这项工作得到了SENSORIA欧洲项目（IST-3-016004）的部分支持。1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.04.01538L. Gönczy等人/理论计算机科学电子笔记175（2007）37由于对异步但可靠的Web服务调用的需求不断增长，中间服务--其中消息的传递可以由底层平台通过适当的重新配置机制来保证--在许多这些标准尽管有各种各样的标准来解决这些可靠性服务属性的规范，但目前行业中只存在非常实验性的解决方案（例如IBM的RAMP-Toolkit [18]或由富士通西门子，日立和NEC领导的联盟的RM 4GS [22]），这些解决方案实际上实现了这些重新配置，以保持所需的可靠性水平。在本文中，我们在概念上遵循[2]，其中开发了一个半正式的平台无关和SOA特定的元模型（本体），以在模型驱动的服务开发过程中捕获各种抽象级别上的服务架构。此外，服务发布，查询和绑定的重新定义由图转换规则捕获[6]，它提供了一种可视化但正式的，基于规则和模式的规范形式主义，广泛用于各种应用领域。这种元建模和图转换规则的组合非常适合服务中间件的基于模型的开发过程本文扩展了[2]中定义的核心元模型（并在第2节中概述）。2）通过一个新的包来实现可靠的消息传递（Sec. 3.2）。此外，我们还提供了新的高级重构原语，用于以图转换规则的形式进行可靠的消息传递（Sec. 4.2）通过集成可靠性技术[16]。最后，我们结合各种分析工具对所提出的规则集进行了形式化验证：首先探索了图文法的状态空间由GROOVE [19]，而生成的图形转换系统被转换为标签转换系统分析器（LTSA）工具可以接受的格式，其中对某些安全属性进行自动化的正式验证。 我们 目的是提供一种通用的方法来捕获SOA的动态容错行为。在本文中，我们使用可靠的消息传递作为案例研究。请注意，我们首先在[10]中以特别的方式通过图转换规则对可靠消息传递的重构规则进行建模。本文通过整合分析工具（第5.3节）正式验证规则，扩展了这种方法。事实上，我们在验证过程中设法在这个初始规则集中找到了概念上的错误，因此本文已经提出了规则的修正版本（在秒4.2）。2个核心SOA元模型面向服务体系结构领域的主要体系结构概念由相应的元模型捕获。“核心”SOA功能的元模型摘录 它基于[2]中提出的元模型，并进行了微小的简化和修改，以使当前论文更好地集中。面向服务架构的核心模型由以下主要元素组成：• 组件是系统中提供服务的基本L. Gönczy等人/理论计算机科学电子笔记175（2007）3739Fig. 1. SOA的核心元模型• 服务是一组具有明确定义的端口和接口的功能。 请注意，在本文中，为了简单起见，我们将服务（和组件）类型和服务实例的概念合并为单个服务（组件）概念。• 端口是可以访问服务的通信• 连接表示运行时两个端口之间的双向通道• 操作是具有输入和输出消息的“原子”操作。可以在同一端口上定义多个操作.• 消息是一组具有预定义子类型的参数，例如请求、响应、服务发布、服务查询和查询结果。 对于目前的文件，我们对待这些消息的抽象层次上，不管他们的实际子类型。然而，我们将在第二节中推导出其他亚型。3.2要求可靠的消息传递。• 服务描述是一个描述符文件，包含所有关于与服务的运行时协作的必要信息，例如端口，操作，消息等的描述。Web服务中可靠消息传递的3个扩展在本节中，在简要概述了捕获现有Web服务技术中的非功能性需求之后，我们将通过可靠消息传递所需的非功能性属性扩展核心SOA元模型，以提供基于模型的解决方案。40L. Gönczy等人/理论计算机科学电子笔记175（2007）373.1现有Web服务技术中的非功能性需求虽然有几个倡议来定义服务的所谓为了通过一个实际而简单的例子来说明非功能属性的建模，在此我们提出了一个基于模型的重构，用于可靠的消息传递以容忍通信故障。由于Web服务的消费者不知道底层网络协议的细节，因此必须在应用程序级别指定消息传递的语义，作为可靠消息传递的要求。这需要一个独立于平台的消息属性表示，这被许多新兴的标准所反映[26，27]。一些流行的应用服务器（如IBM WebSphere或Apache Tomcat）的参考实现是可用的。这些工业标准和倡议通常假设服务提供商与每个客户签订关于服务质量的合同，这些合同是根据诸如平均响应时间、最小吞吐量、消息传递类型等来衡量的。运行时服务实例根据这些契约发送它们的消息，而附加信息，包括这些非功能方面，对应用层是隐藏的。因此，不需要在消费者侧修改原始服务客户端附加信息由感知可靠性属性的组件处理，称为在技术术语中，SOAP信封的报头通过“Reliable Message Endpoints”扩展了一些属性提供者端，然后由客户端的另一个“可靠消息端点”从消息中删除。 由于这些属性的具体格式在消息头中的内容超出了范围，这里我们建模一个抽象的信封概念。在未来，我们计划通过模型转换技术将这些概念映射到现有技术中。3.2服务中可靠消息传递的元模型扩展现在我们扩展[2]的核心SOA元模型，以捕获服务之间可靠消息传递的属性。在丰富了领域元模型之后，我们的长期目标是定义一个相应的UML概要文件，通过以原型和标记值的形式引入领域概念、属性和关系，为特定的应用领域提供定制的UML语言扩展。但是，本文只关注SOA元模型中可靠消息传递的元模型级扩展。我们首先从可靠的SOA元模型中的SOA元素派生一个子类，然后创建一个从子类（例如RelMsgEnvelope）到父类（例如Message）的关联。因此，不可靠的消息传递可能会L. Gönczy等人/理论计算机科学电子笔记175（2007）3741·在[2]中定义的原始SOA重新配置规则执行。 此外，保留原始消息，但通过引入新的关联将其包装到信封中。因此，只需要对[2]的规则进行非常小的扩展，就可以在服务之间传输这些信封，从而正确地记住消息的发送者和接收者SOA元模型的可靠消息传递扩展如图所示。第二章：图二. 可靠性扩展• RelMsgSpecification（简称RelSpec）是一个类，用于指定SOA服务之间可靠消息传递的需求（请参阅关联描述、客户端规范、提供者规范）。属性needsAck是一个布尔值，用于表示是否应向消息发送确认。如果消息的确认到达发送方，则保证消息至少被接收一次。属性filterDuplicates是一个布尔值，表示接收方最多接受和处理一条消息一次。属性timeout是一个计时器约束，它指定发送方在重新传输之前等待消息确认属性maxNumberOfRetrans是一个整数，它对由于缺乏来自接收方的确认而导致的消息可以由发送方重传的次数设置了上限。• RelMsgEnvelope（简称为Envelope）是核心SOA消息的子类，它充当封装要发送的真实消息（wrap）的信封• ReliabilityProperty （ 简 称 RelProp ） 包 含 消 息 的 运 行 时 属 性 ： 属 性numberOfRetrans是信封的序列号，每次重新传输同一消息时，该序列号都会增加1。属性timeElapsed表示自（最后一次）传输 留言该消息的内容也附加到属性（contentOf），因为 消息的重传必须对应用透明• Acknowledgement（简称Ack）是核心SOA消息的子类，表示响应消息而发送的确认·····42L. Gönczy等人/理论计算机科学电子笔记175（2007）37由于这种扩展与现有的标准密切相关，我们计划按照模型驱动的方法将这种高级模型映射到这些标准的实现中：XML描述符的运行时值将从我们模型的属性中派生出来。3.3消息传递在传统的分布式系统中，通信中间件必须保证消息传递的语义。最常见的语义如下：• 至少一次是最弱的一种，要求每个消息都必须到达 接收器至少一次。这并不排除多次发送消息的可能性。• At-Most-Once确保消息• Exactly-Once是前一个的当然还有其他语义，因此我们将使用At-Least-Once作为运行示例，因为这更容易呈现。然而，我们的方法自然也适用于其他交付语义。4基于图转换的可靠SOA消息重构我们现在建议通过图转换规则来描述可靠SOA消息的重构机制（概念上遵循[2]）。4.1图变换概述使用图变换作为形式化规范的一个主要好处捕获重构规则的最大优点是它们是可视化的、直观的，因此它们也可以被服务工程师理解。感兴趣的读者可以在[6]中找到关于图变换的详细理论讨论，在这里我们仅介绍简要介绍一下。此外，图变换允许在特定域中进行动态元建模[12]。将高层（本体）概念可视化为UML类图，将图模式视为UML对象图，将具体模型表示为元模型（类）的实例（对象），结合了精确建模和可视化设计的优点图形转换规则由左手边（LHS）、右手边（RHS）和可选的否定应用条件（NAC）组成。LHS是一种图形模式，由规定规则应用前提条件的强制性元素组成。RHS是一个图形模式，包含应用规则后应该出现RHS中的元素L. Gönczy等人/理论计算机科学电子笔记175（2007）3743\\----LHS中的元素通过转换的执行保持不变，LHS RHS中的元素被删除，而RHS LHS中的元素由规则新创建。否定条件的满足阻止规则在特定匹配上执行。因此，我们遵循单推出方法（SPO）方法[6]，具有负应用条件[11]。一个图文法（GG）由一个起始图和一组图变换规则组成. 图转换系统（GTS）表示由以下生成的状态空间： 图形语法GG的不同状态（即导出的实例图）显示为节点，而边表示由图变换规则的应用引起的状态转换。带有标签r，o的从状态s1到状态s2的边表示通过在匹配o处应用变换规则r可以从图实例s1得到图实例s2。在本文中，当整个规则合并为单个模式时，我们使用图转换规则的紧凑可视化（首先在Fujaba框架[8]中引入并在Groove [19]中使用）。新创建的元素用粗实线（绿色）表示（在编辑器中标记为新建），而删除的元素用蓝色虚线表示（标记为删除）。 交集中的元素 LHS和RHS的元素正常可见（黑色），NAC的元素以粗虚线（红色）显示。本文中使用了一个否定条件来防止规则在相同的匹配上创建无限数量的新元素（例如，在消息传递的情况下，相同的消息只接收一次）。4.2重组规则通过图3中的图形转换（使用Groove符号）捕获的重新配置规则，可以确保至少一次消息传递的可靠消息传递。首先，普通的消息必须被打包到信封中并从信封中包装出来（如在当前可靠消息传递技术的情况下）。因此，消息在发送方侧被打包而不是被发送（图3（g）中的规则closeEnvelope），并且信封在接收方侧接收到它们的内容之前被打开（图3（d）和图3（e）中的规则openEnvelope和openEnvelopeNoAck，其中两个单独的规则取决于消息是否需要确认）。由于最通用的类型用于消息，这些规则将匹配具有可靠性规范的消息类的每个子类的实例。因此，还利用类型化的、属性化的图转换引擎为异步服务调用、发现查询等提供了可靠的消息传递。基 本 交 付 模 式 包 括 AtLeastOnce 、 AtMostOnce 和 ExactlyOnce ， 分 别 由 参 数needsAck和filterDuplicates确定。因此，我们认为在发送端，基本上有两种消息发送模式，这取决于描述消息传递要求的RelSpec对象的needsAck参数的值。 如果该参数为true，则需要可靠的消息发送 对于特定消息，其对应于AtLeastOnce消息传递语义。44L. Gönczy等人/理论计算机科学电子笔记175（2007）37(a) SendMsg（b）ReceiveMsg（c）SendAck(d)OpenEnvelope（e）OpenEnvelopeNoAck(f)RetransmittMsg（g）关闭信封(h)信息丢失（i）(j)成功（k）失败图3.第三章。GROOVE中用于可靠消息传递的转换规则L. Gönczy等人/理论计算机科学电子笔记175（2007）3745抽搐在这种情况下，发送方将等待确认，并且仅当确认在超时间隔内到达时才认为消息传输成功。成功的消息传输的规则（更准确地说，确认的及时到达）如图所示3（j）.另一方面，如果确认没有及时到达（规则超时，图3（i）），则下一个动作（即，要应用的下一个规则）取决于重传消息的数量。如果特定消息的实际重传次数小于允许的次数，则创建Envelope类的新实例，并使用相同的内容和更高的重传次数发送（规则RetransmissMsg，图3（f））。如果不能再次发送相同的消息内容（规则TransmissionFailure的前提条件，图3（k）），则认为消息的传输失败。请注意，如果不需要确认，则在消息发送时不应用任何附加规则，只有核心SendMsg规则与实例图匹配。在接收方，如果需要，消息将被确认（参见规则SendAck在图3（c）），否则核心ReceiveMsg规则被应用（图3（c））。3（b））。已经引入了额外的规则来根据故障模型将故障注入系统。在我们的故障模型中，我们假设消息可能在提交过程中丢失（图3（h）），或者它最终到达但已经发生超时（图3（h））。3（i））。承认也可能丢失。图3的这些故障注入规则是[10]的扩展。 此外，由于我们在之前的工作中使用了更丰富的图模型，因此所有规则都必须手动转换为Groove（参见第二节）。5.2）。最后，在验证过程中，我们还在原始规则集中发现了概念上的错误。例如，我们错误地允许发送方自己接收消息。这些变化已经包含在图中。3 .第三章。5验证可靠的消息传递规则5.1验证工具链转换规则在Groove [19]工具中实现，该工具支持通过以下方式生成状态空间（即图转换系统- GTS）：图形语法使用Groove模拟器，可以从给定的开始图手动检查状态空间以进行验证。虽然这对于GT规范的早期测试是方便的，但在大状态空间的情况下，这不是很有说服力。不幸的是，我们在实验中使用的Groove的当前公开版本（2006年3月）还不支持CTL类属性的验证（最近在[20]中报道）。出于这个原因，我们决定通过在标记转换系统分析器（LTSA，[15]）工具中对生成的GTS进行后处理来验证可靠消息传递的重新配置规则。该工具支持标签迁移系统的安全性、死锁和活性分析.一个需要验证的需求是由一个正常的（需求）过程定义的，它明确地捕获正确和不正确的执行路径（wrt.动作的子集）或属性，46L. Gönczy等人/理论计算机科学电子笔记175（2007）37相应的过程由工具自动生成。对于验证运行，需求过程和系统过程是同时组成的。验证的结果要么是成功的，要么是以导致违反要求的过渡序列的形式提供了一个为了将GTS投影到LTSA的输入格式中，实现了一个翻译器，该翻译器接受由Groove生成的GTS的GXL输入，并相应地创建LTSA进程。此外，由于LTSA分析器总是检查死锁的存在（即使死锁意味着系统的正确终止），我们必须通过引入额外的“重启”图变换规则来保证GTS是循环的这些规则适用于任何配置，并删除有关系统状态的所有信息。或者，这也可以通过在转换器中实现从GTS到LTSA的扩展来完成，以在最终状态上创建循环。5.2特定于Ground的转换规则适应为了将转换规则编码到Groove中（参见图11），3），我们必须在仅支持节点之间的标记边的Groove中对继承，类型和实例化等概念进行建模。因此，节点的类型被建模为自边，并且在继承的情况下我们使用多个边标签。例如，图3（c）顶部的对象具有一种确认类型（简称Ack）， 消息的专门化。具体的属性值（如传输消息的计数器）被实现为节点，链接到它们的容器节点。为了验证规则，必须扩展图语法，以确保它具有无限的生命周期。我们通过系统地修改规则，确保可以从任何后续状态到达起始状态。首先，创建了两个新规则，用于在消息传输（成功或失败）后恢复系统的启动状态。其次，通过三个辅助变换，删除了消息、信封、信封等不必要的元素，保持了状态空间的有限性。第三，所有其他规则都由包含MessageProperty类的success属性的NAC扩展为了防止这些规则与初始化SE同时执行顺序。5.3验证属性我们确定了以下（非排他性）可靠消息传递的重要要求列表：• 消息的传输要么成功，要么失败（但提交具有明确的结果）。• 当超过最后一个可传输消息实例• 传入消息仅在确认后读取（如果确认L. Gönczy等人/理论计算机科学电子笔记175（2007）3747(a) 变速器（b）故障(c)确认图四、属性的自动机（-1表示错误状态）需要）。• 正确管理同一端口的多个消息（到相同或不同端口），即，它们的运行时属性被逐个处理• 仍然可以发送和接收正常（不可靠）消息。在LTSA中形式化这些需求时，我们遇到了两个主要问题。一方面，由Groove生成的GTS仅包含作为标签的应用规则，但不提供关于出现的信息。出于这个原因，我们只能捕获那些与消息的身份无关的需求。在一些情况下，实际上只有一种弱化形式的要求得到了验证，解决这个问题在我们看来，为匹配提供信息是Groove未来改进的一个有趣方向另一方面，LTSA提供了一种有限的方法来检查活动属性，因此，我们的注意力主要集中在验证可靠消息的安全属性。结合使用这两个工具的主要好处是可以轻松生成可用状态和自动检查属性。前面的要求以LTSA过程/属性的形式进行了解释和形式化（见图1）。（4）如下。• 消息的传输要么成功，要么失败：转换规则Success，Failure中的确切一个应用于每个路径的重新启动状态（图1）。4（a））。• 当最后一个可传输消息实例的确认超时被超过时，传输被认为是失败的（图1）。4（b））。• 传入的消息仅在被确认后才被读取，即SendAck规则的应用先于OpenEnvelope规则 的 应 用 注 意 ， 如 果 不 需 要 确 认 ， 则 不 违 反 该 属 性 ， 因 为 改 为 应 用OpenEnvelopeNoAck规则（图1B）。4（c））。48L. Gönczy等人/理论计算机科学电子笔记175（2007）37通过仔细选择初始模型来捕获小但典型的配置，我们能够验证我们的重新配置规则是否满足这些要求。我们相信，这些模型是最小的，但有代表性的配置，可以扩展，如果这没有提出一个冲突的状态空间生成的限制。 另一方面，我们最初的一些预期 在验证期间为false（例如，消息丢失总是会导致超时）。我们从可靠消息传递中使用的重新配置规则的验证案例研究中学到的主要经验教训如下：• 高级与低级图模型和规则：我们能够（手动）翻译丰富的图转换规则和模型（如[10]中使用的继承，类型，属性等）。使用相对简单的建模技巧将其转换为较低级别的验证模型（在Groove中使用）。• 在Groove中测试： 小概念性的错误已经在《规则》中得到确认，[10]通过手动检查生成的GTS以获得较小的示例。然而，这样的人工检查，以确定一个属性的正确性是不可行的大状态空间。• LTSA中的验证：LTSA中的自动后处理是验证有意义的安全属性的可行解决方案，但由于Groove生成的GTS中缺乏身份信息，因此存在明显的局限性6相关工作该领域的相关工作通常集中在描述服务的非功能属性，或者通过图转换对面向服务架构的动态方面进行建模。我们的工作在概念上遵循[2]的方法来指定SOA中的服务。[3]的作者描述了图转换在行为Web服务规范的运行时匹配中的应用。在[13]中，Web服务的一致性测试是基于图转换的，重点是自动化测试用例生成。然而，这些作品都没有讨论可靠消息传递的各个方面。我们的目标是通过扩展元模型和转换规则来利用这种方法的好处。图变换在[7]中被用作使用代数框架CommUnity的动态建筑重构的规范技术。Hirsch在[14]中使用超图上的图转换来指定给定架构风格中组件，重构和移动性之间的运行时交互。但是，这两种情况都没有解决SOA中的可靠消息传递问题。LTSA[15]已经成功地应用于[9]中以规范形式给出的业务流程的形式分析，但可靠的消息在这些文件中没有考虑在未来，我们计划研究使用其他验证工具来验证图语法。一个主要的候选者是Augur [21]，它使用展开技术来L. Gönczy等人/理论计算机科学电子笔记175（2007）3749导出GTS中可能轨迹的有限近似在[4]中，使用图形语法对故障行为进行了详细说明和分析。虽然这种方法与SOA没有直接关系，但它可以作为我们研究中引入其他可靠性方面的起点。可靠消息传递在其他文献中得到了验证（例如[1]），我们的技术差异主要在建模层面，更接近于通常的SOA描述，因此更适合应用于SOA中容错机制的验证。最后，在工业领域，存在现有和新兴的规范和技术，如[26，27]。但是，它们的使用仍然是临时的，并且没有基于模型的设计时支持可用于可靠的消息传递。7结论在本文中，我们首先提出了对[2]的核心SOA元模型的扩展，一种捕获重构机制的技术，以增强更健壮的SOA中间件的开发。图转换规则捕获了SOA中可靠消息传递的重构规则首先利用Groove生成图文法的状态空间（以图迁移系统的形式），然后将其转换为带标签的迁移系统，利用LTSA分析工具对正确性要求进行形式化验证，从而作为未来的下一步，我们计划专注于弥合抽象重构规则与可靠Web服务的现有实现技术之间的差距。经过正式验证的一套重新配置规则将明确作为此活动的良好起点。我们的长期目标是在各种现有平台上直接基于正确的动态重构机制自动实现可靠的消息传递。引用[1] P. P. Katoen，T.Ruys和J.崔特曼有界重传协议的建模与验证。1996年，斯洛文尼亚，COST-247系统设计应用形式方法国际研讨会论文集。[2] L. 巴雷西河 He ckel，S. ThéoneandD. Vo，基于风格的设计和面向服务的建筑的改进。 发表在Journal ofSoftware and Systems Modelling，2006。[3] A. Cherchago和R.海克尔使用条件图转换规则的Web服务规范匹配。在2004年国际图变换会议论文集，LNCS Vol.3256.中，施普林格，pp. 304-318[4] F. L. 多蒂湖Ribeiro和O.M. 多斯桑托斯。使用图形语法对故障行为进行规范和分析。在具有工业相关性的图变 换的 应用 中， 第 二次 国 际研 讨会 ，AGTIVE 2003， 美国 ， 第一 卷。 第 3062 章 ，你 来了 ？120-133Springer，2003年。[5] DublinCore Metadata Initiative，2006年。http://dublincore.org/[6] H.埃里格河Heckel，M. Kor Kang，M.洛湖里贝罗A. Wagner和A.科拉迪尼图变换的代数方法，第二部分：单 推 出 法 及 与 双 推 出 法 的 比 较 。 在 Handbook of Graph Grammars and Computing by GraphTransformation，卷I：基础，pp.247-312 世界科学，1997年。50L. Gönczy等人/理论计算机科学电子笔记175（2007）37[7] M. Wermelinger和J.L.菲亚代罗软件体系结构重构的图变换方法。Comp.的科学进展，44（2）：133[8] T. Fische r，J. 尼埃雷湖我的意思是，我的意思是，我的意思是。 张文龙，“基 于 UML 和 Java 的图 形转 换语 言”， 《图 形转 换理 论与 应 用》 （ 1998年 ）， 第一 卷 。LNCS 1764， 2000，Springer。[9] H.福斯特，S。Uchitel，J. Magee，and J. Kramer. 基于模型的Web服务组合验证。在第18届IEEE国际自动化软件工程会议（ASE 2003），加拿大，pp。152-163. IEEE计算机学会，2003年。[10] L. Güonczy，D. Varo：面向服务的可靠消息传递模型和Archit ectur s，InProc. 内部Web服务建模和测试研 讨 会 （WS-MATE 2006）。地出现。[11] A.哈贝尔河Heckel和G.坦策具有否定应用条件的图文法。Fundamenta Informaticae，26（3-4）：287313，1996.[12] J.H. Hausmann，Heckel，R.，Lohmann，M.：基于模型的Web服务发现，在IEEE Int.Web服务会议（ICWS），2004年6月 6-9日，美国，[13] R. Heckel和L.马里亚尼. Web服务的自动化一致性测试。在Proc.of 8th Int.Conference on FundamentalApproaches to Software Engineering（FASE 2005），vol.3442 of LNCS，Springer，pp. 34比48[14] D. 赫希软件架构风格的图形转换模型。博士论文，布宜诺斯艾利斯大学计算系，2003年。[15] 标签转换系统分析器（2.2版）http://www-dse.doc.ic.ac.uk/concurrency/ltsa-v2/index.html[16] J. Laprie，B.兰德尔角陈晓，安全计算的基本概念和分类，安全计算学报，（2001），第1卷，第1期。（2004）pp.11-33[17] 对象管理组。 模型驱动架构。http://www.omg.org/mda[18] ReliableAsynchronousMessageProfile （RAMP）Toolkit，IBMalphaworks。http://www.alphaworks的网站。ibm.com/tech/ramptk[19] A. Rensink，Groove模拟器：状态空间生成工具。在Proc. of Application of Graph Transformations withIndustrial Relevance（AGTIVE'03），2003，LNCS Vol.3062，Springer，pp. 479-485.[20] Kastenberg H.，和Rensink A. GROOVE中的模型检查动态状态。在2006年Springer-Verlag出版的LNCS第3925卷的第13届软件模型检查国际研讨会（SPIN'06）的论文中，出现。[21] B. Küonig和V. 我是奥齐乌拉一种用于分析语法变换系统的语法分析工具。EATCS公报，卷。87：pp. 126[22] RM4GS参考指南，版本1.0，FUJITSU LIMITED，Hitachi，Ltd.和NEC公司，2004年。http://xml.coverpages.org/rm4gs20041125-reference.pdf[23] 面向服务的覆盖计算机软件工程（SENSORIA）欧洲项目IST-3- 016004。http://sensoria.fast.de[24] Web服务架构，2004年。http://www.w3.org/TR/ws-arch/[25] Web 服务建模本体（WSMO ），W3C 成员提交，2005 年。http://www.w3.org/Submission/2005/SUBM-WSMO-20050603/[26] Web 服 务 可 靠 消 息 传 递 协 议 （ WS-ReliableMessaging ） IBM 、 Microsoft Corporation ， Inc. 和 TIBCOSoftware Inc.2002年。[27] Web Services Reliable Messaging TC WS-Reliability 1.1 Committee Draft 1.086 ， OASIS OpenConsortium，2004。