理论计算机科学电子笔记105（2004）109-118www.elsevier.com/locate/entcs在跟踪马库斯·文茨克1电信部门TechnischeUniversitéatHamburrg-Harburrg德国汉堡摘要本文通过提出一种灵活的规范化技术SXQT与自动验证相结合，这是一种检测不一致性的直接方法，从而有助于Web服务的互操作性。SXQT通过指定对Web服务协议的单独需求，即其SOAP消息和行为（包括SOAP模块），允许不同级别的抽象。自动验证通过将出现的消息序列与协议的规范进行比较来检测不一致性关键词：自动验证，编排，规范化技术，SXQT，Web服务，XQuery1介绍规范对于Web服务应用程序的互操作性起着至关重要的作用。它们描述了Web服务提供者与其客户端（Web客户端）之间的协议。在不同企业中的独立实施需要精确的规范，以允许无危害的互通，但仍为广泛的实施留下空间。通用的Web服务描述语言（WSDL）[16]只允许稀疏的规范。它描述的是交换消息的类型和结构.预期的协议行为，例如所需的消息排序，无法指定，但对于成功的互通至关重要。1电子邮件：venzke@tu-harburg.de1571-0661 © 2004由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2004.05.004110M. Venzke/Electronic Notes in Theoretical Computer Science 105（2004）109协议行为可以在BPML [2]和BPEL 4WS [20]中指定。这些非常详细地指定了Web服务，允许执行规范。从这个意义上说，它们更像是编程语言，而不是特定语言。实现者被限制将规范编译成实现，没有设计决策的空间（cp。[17]）。BPML和BPEL4WS以及WSCL [3]和WSCI [1]不允许指定SOAP模块[12]。SOAP模块是通用的、基础设施相关的协议，其数据单元在SOAP报头中传送。示例是WS-* 协议[18]。为了开发Web服务的协议，应用程序特定的部分（在SOAP主体中传递）由所需的使用上面提到的指定技术，这些不能被指定，因为它们的模型是基于WSDL因此，没有SOAP头的概念，其内容无法指定。本文提出了规范化技术SXQT，它允许规范化应用程序特定的协议、SOAP模块以及它们之间的关系。可以选择不同的抽象级别，以便仅指定Web服务提供商及其客户端之间交互所需的那些要求尽管有精确的规范，但仍然存在由于不一致的实现而导致不兼容的风险。这个问题经常通过测试实现来解决不幸的是，测试只能确保有限数量的测试用例的一致性。此外，如果误解了规范，开发人员将不会发现导致的不符合项。程序验证不仅仅是形式上证明实现但为非平凡的实现找到这样的证明是极其复杂的。作为对这个问题的贡献，本文提出了自动验证，它允许检测出现的消息序列的不一致性。当用于测试时，不一致性的检测与开发人员的理解无关。在生产中永久使用，它是一种直接的方法来检测每一个发生的违规。SXQT是为了方便自动验证而开发的。2SXQTSXQT （ Specifications using XQuery expressions on Traces ） 基 于 约 束XML文档的结构和值的predates。每个对结构和值的要求都被单独表示为一个谓词，如果满足了要求，则返回true。为了指定协议这一概念与霍尔的模拟具体化类似M. Venzke/Electronic Notes in Theoretical Computer Science 105（2004）109111事件序列[13]。2.1迹线时间顺序到跟踪的转换是基于观察Web服务提供者或客户端发送或接收的这些事件被认为是原子性的，没有持续时间，不能与其他事件同时发生。不考虑绝对时间。一个概念性的观察者按照观察的顺序记录事件，直到轨迹中的某个时间点，如图1所示。它从一个空的跟踪开始，一个只包含根元素的XML文档。对于每个事件，记录SOAP消息和其他可观察的元数据。它作为子元素追加到跟踪的末尾。由此产生的数据结构如图2所示，描述了一个包含四个事件的轨迹Fig. 1.观察者记录轨迹... /. /env：信封>. /tra：在线留言>. /tra：在线留言>图二. 示例轨迹使跟踪成为XML文档是一个显而易见的选择，它允许使用相同的技术规范时间顺序和数据结构。的112M. Venzke/Electronic Notes in Theoretical Computer Science 105（2004）109XML的层次特性允许将SOAP消息的层次嵌入到跟踪的单个层次中。不需要额外的形式主义来表示时间顺序。此外，以相同的方式表示时间顺序和消息结构，可以使用相同的技术来指定它们SXQT为此使用谓词。2.2SXQT表达式SXQT 的谓词称为SXQT 表达式。SXQT 表达式将跟踪映射为true 或false。它需要被设计为返回true，如果它所描述的请求由跟踪填充。它用XML查询语言（XQuery）[6]表示，后者提供了它的语法和语言的语义。XQuery非常适合Web服务领域的规范。在[10]中提供了形式语义。作为万维网联盟（W3C）的标准化组织和XML数据库SQL的继承者，Web服务领域的未来开发人员将了解它。工具将可用。它提供了处理XML结构化数据和表达谓词的方法。用户定义函数允许抽象和重用部分表达式.最后，一个标准库[14]包含许多对SXQT表达式有用的标准函数。为了方便谓词的构造，SXQT提供了一个额外的库。它的函数简化了SXQT表达式的构造，隐藏了跟踪和SOAP消息的结构这也增加了可读性。2.3SXQT表达式作为说明，下面将讨论示例SXQT表达式2。它描述了WS-Transaction [7]中使用的两阶段提交协议的消息排序需求，该要求指出，如果观察到回滚消息，则之前必须没有观察到同一事务的提交消息。每百万美元在opr：restrict（opr：tr（），xs：QName（“wsat：Rollback”））中，满足empty（opr：restrict（myfn：EventsInTxBefore（$m），xs：QName（“wsat：Commit”）图三. 示例SXQT表达式与大多数SXQT表达式一样，图3中的示例使用XQuery2 更多的例子在[22]。M. Venzke/Electronic Notes in Theoretical Computer Science 105（2004）109113对于跟踪中的特定类型的消息。在本例中，谓词必须为true的是Rollback消息，即在跟踪中没有属于同一事务的较早的在关键字in之后，确定所有Rollback消息的顺序跟踪中的所有消息都可以通过SXQT的函数opr：tr访问这些限制为使用函数opr：restrict的回滚消息。对于每个Rollback消息，关键字satisfies之后的谓词将使用引用它的变量$m进行评估。它将被赋予函数myfn：EventInTxBefore，该函数确定同一事务中的早期消息。这些仅限于提交消息。由于要求在回滚消息之前拒绝提交消息，因此不应返回任何消息。这是用XQuery的标准函数empty检查的函数myfn：EventInTxBefore是专门为指定WS-Transaction而定义的。通过抽象部分表达式来确定同一事务中的早期消息，它大大提高了可读性，并允许在多个SXQT表达式中重用。可以为其他规范定义类似的函数，以确定Web服务和一个Web客户端之间的对话的所有消息，以便于指定对话的动态。函数myfn：EventInTxBefore将SOAP模块与协议的应用程序特定部分相关联。WS-Transaction的消息需要在SOAP头中携带事务标识符。 函数使用它来确定属于同一事务的消息。通过将SOAP消息视为一个整体，与SOAP模块的关联成为可能。一种基于WSDL端口类型的模型不会允许这样的事发生2.4个性化需求单独表达需求是SXQT的主要优势。它只允许指定互操作所需的需求。不同的部分可以独立地表达他们的需求，可能只覆盖单个SOAP模块或协议的应用程序特定部分。SXQT example可以与WSDL结合使用，描述WSDL没有表达的需求基于自动机的规范不允许单独表达需求。一个单一的，封闭的模型（自动机）必须构建，以满足所有的要求。虽然这使实现变得容易，但这阻碍了对各个需求的推理。此外，添加或挂起一个需求需要重新构建整个模型。通过单独表达需求，SXQT允许关注这些需求，并使需求的添加和挂起变得微不足道。114M. Venzke/Electronic Notes in Theoretical Computer Science 105（2004）109不同的要求也允许不同的抽象水平。只有特定目的（例如互操作）所需的需求才需要表达。方案开发可以从主要需求开始。在更好地理解之后，可以添加其他要求。一个规范的SXQT表达式可能来自不同的各方。通过这种方式，每一方都可以独立地指定其对协议的要求。标准要求一旦正式化，就被添加到许多规范中。一个例子是WS-Coordination [8]的要求，即消息需要在其SOAP头中包含协调上下文。这是所有使用WS-Coordination（如WS-Transaction）的协议所必需的。该要求可能仅正式化一次，然后添加到所有这些协议的规范中。通过这种方式，SXQT可以用来指定独立于特定Web服务协议的SOAP模块。SOAP模块的需求被描述为SXQT表达式。需求可以包括对其他SOAP模块或SOAP主体的假设。当指定Web服务的协议时，所需SOAP模块的所有SXQT表达式都被添加到其规范中。SXQT表达式可以与WDSL结合使用，以避免重复指定。WSDL不能被SXQT取代，因为它是一个事实上的标准，很多工具都可以读取WSDL，例如。代理生成器。此外，它还允许更简洁地说明一些需求，例如SOAP消息的结构和类型。因此，只有那些没有用WSDL表达的需求才应该用SXQT表达式表达。应该使用可扩展性元素将它们添加到WSDL文档中，WSDL3允许扩展。扩展的WSDL文档，描述了Web服务如果实现不符合规范，则仍然存在不兼容的风险。该问题与所使用的规范技术无关本文通过提出自动验证来解决这个问题，这使得检测不一致性变得简单。3自动验证自动验证是检查发生的消息序列是否符合协议规范的过程。关键的想法是直接3见[9]，第6节。M. Venzke/Electronic Notes in Theoretical Computer Science 105（2004）109115将观察到的消息序列与规范进行比较。 然后，可以将不一致性通知给开发人员、管理员、用户或实现。这与用于无副作用程序的[4]第四章。 SXQT的开发非常适合此目的。自动验证支持开发人员创建一致的实现。它可以从第一个原型开始应用，即使规范处于早期状态并且只包含主要需求。在测试时，它使开发人员不必决定实现是否按照指定的方式运行。即使不符合项源于开发人员对规范的在生产环境中永久使用时，开发人员会被告知任何违规行为，或者知道从未发生过。在长时间的一致性之后，生产环境中发生的偏差是对开发人员的一个提示，即协议可能已经更改，Web客户端需要更新。不同企业中Web服务提供者和客户端的自主演化Web客户端只需要更新，如果它可以观察到违反它实现的规范。因此，根据此规范进行验证允许检测需要更新的协议更改。自动验证还允许保护Web服务提供者免受不一致的、危害性的SOAP消息的影响。这样的消息可能会出现形式的实现错误或恶意用户，谁试图入侵Web服务提供商。如果没有执行所有必要的检查，这可能会危及提供商。使用自动验证，可以更可靠地执行检查。然后，在将消息传递到Web服务提供者之前，对消息进行验证。 在不符合的情况下，它不会被传递，而是用错误消息回答Web客户端3.1验证器执行自动验证的实体称为验证器。如图4所示，它由一个观察者和一个核心验证器组成观察者能够观察Web服务提供者或客户端发送或接收的SOAP消息。它可以被看作是SXQT的概念观察器的具体实现因此，它将SOAP消息按照观察到的顺序记录到跟踪中（cp。第2.1节）。核心验证器检查跟踪所表示的消息序列是否符合规范。如[22]中所讨论的，验证器在何处以及如何观察消息方面存在差异。4 我们在[21]和[22]中进行了比较。116M. Venzke/Electronic Notes in Theoretical Computer Science 105（2004）109见图4。 验证器的基本结构当验证被执行时，观察可以发生在Web服务或客户端。观察者可以在单独的进程中实现为HTTP代理[11]，或者分别在Web服务提供者或客户端的进程中实现。当观察到一条消息时，它可能会被立即验证，或者只记录到跟踪中以供以后验证。后一种方法对性能的影响较小，但并不适用于所有使用场景。3.2根据SXQT质量标准进行验证SXQT使得自动验证简单明了，并且在很大程度上可以使用标准软件来实现。对SXQT表达式的验证可以使用标准的XQuery处理器执行，对XML模式定义的验证使用标准的模式验证器。针对SXQT表达式的验证的直接性源于SXQT要验证所观察到的跟踪是否符合SXQT表达式，只需要使用跟踪作为参数对表达式进行求值。为了一致性，这必须返回true。由于SXQT表达式是XQuery表达式，因此可以使用不同供应商提供的标准XQuery 处理器执行计算（参见[15]）。这有助于验证器对于扩展的WSDL文档，验证器还必须考虑用WSDL表示的这包括XML Schema [19]中用于定义SOAP消息的数据结构的定义针对后者的验证可以使用不同供应商提供的模式验证器来执行（参见[19]）。M. Venzke/Electronic Notes in Theoretical Computer Science 105（2004）1091174结论自动验证和SXQT是对Web服务互操作性的贡献。规范技术SXQT允许在不同的抽象级别上指定协议的SOAP消息和所需的需求被单独描述为称为SXQT表达式的谓词。这些可能来自表达其要求的不同方，通过将时态排序转换为XML数据结构来描述行为，从而允许使用相同的技术（谓词）来指定消息结构和时态排序。考虑整个SOAP消息使得能够指定SOAP模块，包括对其他SOAP模块和SOAP主体的假设。选择XQuery使Web服务领域的开发人员易于学习SXQT。SXQT非常适合自动验证，这是一种检查出现的消息序列是否符合规范的直接方法。它通过检测早期原型或最终实现的测试环境或生产环境中的不一致性，引用[1] Arkin，Assaf，et.例如，Web服务编排接口（WSCI）1.0. W3C Note.万维网联盟（W3C），2002年8月。http://www.w3.org/TR/2002/NOTE-wsci-20020808/（访问日期：8（2003年12月）[2] Arkin，Assaf，业务流程建模语言。在最后一次通话中。业务流程管理倡议（BPMI.org），2002年。http://www.bpmi.org/bpml-spec.esp（访问日期： 13 （2003年2月）[3] Banerji，Arindam，et.例如，Web服务会话语言（WSCL）1.0. W3C Note.万维网联盟（W3C），2002年3月。http://www.w3.org/TR/2002/NOTE-wscl10-20020314/（访问日期：8（2003年12月）[4] Blum，Manuel和Kannan，Sampath，设计检查他们工作的程序。In：Journal of theACM，Vol. 42，Nr. 1，S. 269-291，Januar 1995. ftp://ftp.cis.upenn.edu/pub/kannan/jacm.ps.gz（2002年12月21日查阅）[5] Box，Don，UnderstandingGXA. 微软公司，2002年7月。http://msdn.microsoft.com/library/en-us/dngxa/html/understandgxa.asp（2003年12月15日[6] Boag，Scott，et.例如，XQuery 1.0：一种XML查询语言。W3C工作草案。万维网联盟（W3C），2003年11月。http://www.w3.org/TR/2003/WD-xquery-20031112/ （访问日期： 11 （2003年12月）[7] Cabrera，Felipe，et. 例如，Web服务事务（WS-Transaction）。IBM Systems，国际商业机器公司，微软公司，2002年8月。http://www-106.ibm.com/developerworks/library/ws-transpec/（2004年2月6日查阅）[8] Cabrera，Felipe，et. 例如，Web服务协调（WS-Coordination）。IBM Systems，International Business Machines Corporation，Microsoft Corporation，2003年9月。http://www-106.ibm.com/developerworks/library/ws-coor/（2004年2月6日查阅）118M. Venzke/Electronic Notes in Theoretical Computer Science 105（2004）109[9] Chinnici，Roberto，et.例如，Web服务描述语言（WSDL）2.0版第1部分：核心语言。W3C工作草案。万维网联盟（W3C），2003年11月http://www.w3.org/TR/wsdl20/（2004年2月6日查阅）[10] Draper，Denise，et.例如，Xquery 1.0和Xquery 2.0形式语义。W3C工作草案。万维网联盟（W3C），2003年11月。http://www.w3.org/TR/2003/WD-xquery-semantics-20031112/（访问日期：11（2003年12月）[11] 菲尔丁R.，et. 例如，超文本传输协议RFC 2616。互联网工程任务组（IETF），1999年6月。http://www.ietf.org/rfc/rfc2616.txt（访问日期： 23 （2003年7月）[12] Gudgin，Martin，et.例如，SOAP版本1.2第1部分：消息传递框架。W3C推荐。万维网联盟（W3C），2003年6月。http://www.w3.org/TR/2003/REC-soap12-part1-20030624/（访问日期：2003年7月18日）[13] Hoare，C.A.R，Communicating Sequential Processes。普伦蒂斯-霍尔，伦敦，1985。[14] Malhotra，Ashok，et.例如，Xquery 1.0和Xquery 2.0函数和运算符。W3C工作草案。万维网联盟（W3C），2003年11月。http://www.w3.org/TR/2003/WD-xpath-functions-20031112/（2003年12月11日查阅）[15] Marchiori，Massimo，XML Query（XQuery）.网站万维网联盟（W3C），2003年12月。http://www.w3.org/XML/Query（访问日期： 12 （2003年12月）[16] Marsh，Jonathan，Le Haught，Philippe，Web服务描述工作组。网站万维网联盟（W3C），2003年12月。http://www.w3.org/2002/ws/desc/ （访问日期： 12 （2003年12月）[17] 梅雷迪思，L.G.，Bjorg，Steve，Contracts and Types。载于：ACM通信，第46卷，第10号，2003年10月。[18] Microsoft，Web服务规范索引页。网站微软公司，雷德蒙德，2003年。http://msdn.microsoft.com/library/en-us/dnglobspec/html/wsspecsover.asp（查阅日期：2003年12月10日）[19] Sperberg-McQueen，C. M.，Thompson，Henry，XML Schema.网站万维网联盟（W3C），2003年11月。http://www.w3.org/XML/Schema（访问次数：12） （2003年12月）[20] Thatte，Satish，et.例如，Web服务的业务流程执行语言版本1.1。IBM Systems，InternationalBusiness Machines Corporation，Microsoft Corporation，SAP AG，IBM Systems，2003.http://www-106.ibm.com/developerworks/library/ws-bpel/（访问日期：30（2004年1月）[21] Venzke，Marcus，Web服务的自动验证。在：第八届解百纳激进研讨会的电子会议记录。2003年10月http://www.newcastle.research.ec.org/cabernet/workshops/radicals/（查阅日期：2004年2月6日）[22] Venzke，Marcus，Spezi fikation von interoperablen Webservices mit XQuery.博士论文。Techn ischeUniverrsitüatHamburg-Harburg，2003.http://doku.b.tu-harburg.de/volltexte/2004/51/（访问日期： 6 （2004年2月）
我的内容管理
收起
我的收益 登录查看自己的收益
我的积分
登录查看自己的积分
我的C币
登录后查看C币余额
我的收藏 
我的下载 
下载帮助 
