Web服务的分发和协调是基于语义验证工具包的新方法

理论计算机科学电子札记105（2004）11-20www.elsevier.com/locate/entcsWeb服务作为分发和协调基于语义的验证工具包的新方法1Michael Baldamus2 Jesper Bengtson瑞典乌普萨拉大学信息技术系法拉利3Diparti medInformati ica，itativersitadiPisa，ItalyRoberto Raggi罗伯托·拉吉4，5Trolltech AS，奥斯陆，挪威摘要正式验证工具包通常相当特殊，如果将不同的相关工具包相互比较，则具有互补的功能。因此，建议将不同的相关工具包纳入共同环境。这种集成的潜力是正式验证工具包是基于语义的事实的直接结果，因为它们是很好理解的数学理论的实现。我们认为，Web服务可以作为一个新的平台，解决更实际的问题，与：一方面，服务集成一般肯定是Web服务范式的一个重要组成部分。此外，Web服务促进了分布式和开放式集成，这适合正式验证社区的分散和动态。此外，类目录技术有助于解决正式方法工具集成中的协调问题。关键词：Web服务，工具集成，形式验证，分布，协调1欧洲联盟PROFUNDIS项目支助的工作，合同号IST-2001-33100。2http://user.it.uu.se/~michaelb3http://www.di.unipi.it/~giangi第rraggi@trolltech.com5Roberto Raggi在他与Dipartimento di1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.02.02412M. Baldamus等人/理论计算机科学电子笔记105（2004）111介绍在过去的几年中，万维网上的分布式应用程序，简称Web，如电子商务，文件共享，已经获得了广泛的普及，在设计和控制它们时，对进化范式的需求越来越大。统一的机制已经被开发用于处理涉及大量物理上分布的并且自主操作的这些发展已经开始围绕一个范例进行整合，在这个范例中，Web被用作服务分发者。从这个意义上说，服务不是一个单一的Web服务器，而是一个可以通过Web获得的组件，其他人可以使用它来开发其他服务。从概念上讲，Web服务是Internet中的独立组件。每个Web服务都有一个可通过标准协议访问的接口，同时描述服务的交互功能。Web上的应用程序是通过组合和集成Web服务来开发的。而且，没有Web服务预先知道与其他Web服务可能发生什么交互.我们在这里认为，这种范式可以卓有成效地应用于集成正式验证工具包的问题。我们的动机是以下三点：• 整合相关的正式验证工具既有必要，也有好处，因为尽管它们是相关的，但它们通常相当特殊，同时至少部分互补。• 集成有一个良好的概念基础，因为验证工具包是基于语义的，因为它们是很好理解的数学理论的实现。因此，原则上很容易匹配相关工具的接口（部分），以便它们可以一起工作• 当然，连接不同语法输入和输出格式等的问题仍然存在。然而，这种一体化也存在问题，因为正式的核查界非常分散，同时又高度动态。此外，可用于处理可移植性甚至可卸载性的资源通常是有限的。这些观察结果之前已经提出过，实际上已经提出了验证工具包集成的其他概念（例如[4]）。然而，Web服务是解决这个问题的我们的做法是分散的，从而将问题转移到协调领域。出于两个基本原因，这种处理问题的方式似乎是自然的：对于我来说，如果没有人在我的地盘上，M. Baldamus等人/理论计算机科学电子笔记105（2004）1113(i) 分发解决了正式方法社区不愿意在工具集成方面参与任何集中式的电子商务的问题。 有些工具是可移植的，但另一些工具不是或仅在有限程度上是可移植的，甚至可供下载，并且由于各种原因，这种情况不太可能很快改变。与集中式方法相比，分布式也有一些内在的优势，例如可用性、可重构性和开放性。(ii) 从协调的角度来看，分布式工具集成似乎是最好的，因为我们的目标是我们所说的深度集成：应该有自动的方法将属于任何验证运行的子任务分配给最适合解决它们的节点。这反过来又需要一个平台和一种语言，允许用户在不同的抽象层次上指导应该在哪里做什么。这一要求几乎可视为协调的同义词。浅集成只意味着用户可以在不同的工具之间进行选择，以整体解决任何验证问题。我们当前的重点是验证移动流程的工具包（例如，[9，10，16]）在π演算[13]和相关的更高级别的工具的意义上，用于验证安全协议（例如，[2，14]）。这里介绍的工作的一个主要思想是使用XML、WSDL和SOAP等标准，将基于语义的验证工具包作为Web服务提供另一个主要思想是建立目录来发布这样的Web服务。在此基础上，我们将能够证明验证工具是基于语义的，因为这一特性应该允许我们为服务提供强大的自动化匹配工具。因此，验证网络服务加上自动验证网络服务最重要的是，有一个验证脚本工具，以便用户能够指定如何执行任何验证运行中的子任务。除了目前的原型，我们设想，一个重要的作用，最终将发挥嵌入在基于语义的目录中的交易功能。具体来说，在证明脚本中应该有不同的抽象层次，即面向目标，面向算法，面向工具和面向节点的层次。本文的其余部分介绍了一个环境的原型，该环境通过Web将不同的验证工具集成和协调为服务分发器。核查环境的开发是在欧洲联盟全球计算倡议的Profundis项目（见网址http://www.it.uu.se/profundis）内进 行 的 。 出 于 这 个 原 因 ， 我 们 称 之 为 Profundis WEB ， 简 称PWeb。14M. Baldamus等人/理论计算机科学电子笔记105（2004）112预赛2.1Web服务Web服务由一个接口组成，该接口描述通过Internet协议栈上的消息交换可访问的操作。Web服务的描述必须涵盖与之交互所需的所有细节：消息格式、传输协议等等。因此，Web服务是基于Internet标准的分布式系统的编程技术。然而，Web服务不仅仅是分布式系统的另一种基于对象的范例。事实上，他们提倡面向服务的编程风格，这与标准的用户到程序风格不同[12，17]。面向服务的编程隐喻通常以发布、查找和绑定周期为特征为了以可互操作的方式发布-查找-绑定，Web服务依赖于一组网络协议。该协议的构建块是简单对象访问协议（SOAP）[3]。SOAP是一种基于XML的消息传递协议，定义了远程过程调用的标准机制。Web服务描述语言（WSDL）[6]定义了接口和详细的服务交互。通用描述、发现和集成（Universal Description Discovery and Integration，缩写为EDP）协议支持发布和发现工具[18]。最后，利用Web服务业务流程执行语言（BPEL4WS）[8]通过组合其他Web服务2.2验证工具包多年来，一些基于语义的验证工具包已经被设计和试验，以正式解决软件开发中提出的一些问题。例如，Concurrency[7]是由爱丁堡大学开发的，它对通信系统的微积分（CCS）进行分析。在乌普萨拉大学开发的MobilityQuestionnaire（MWB）[16]也进行了类似的分析，但基于π演算。历史依赖自动机实验室（HAL）[9]支持对表达π演算主体行为属性的逻辑公式进行验证。大多数基于语义的验证环境都是相互独立开发的，并且无法保证它们可以互操作，因此某些属性的验证是工具包之间协作的结果。在验证社区中，处理集成问题的标准方法是提供基于通用格式的协调基础设施。FC2形式[1]是这种方法的一个说明性例子的M. Baldamus等人/理论计算机科学电子笔记105（2004）1115FC2格式提供了一种表示自动机的语言。自动机以FC 2格式通过一组表来表示，这些表保存有关状态名称、弧标签和状态之间的转换关系的信息。FC2允许验证工具包之间的互操作性。电子工具集成平台（ETI）倡议[4]采用了不同的方法ETI是一个基于网络的基础设施，用于验证工具包的交互式实验。协调中间件（HLL）提供了PWeb提出自己作为一个实验，以解决集成问题，利用Web服务。PWeb原型实现被设想为支持对π演算的某些方言中指定的系统行为的推理。PWeb集成和协调作为Web服务提供的一些验证工具包的设施。MWB和HAL是PWeb的两项服务。下面，我们简要介绍PWeb其他服务的主要特点。信任TRUST工具箱[15，14]依赖于一种精确的符号归约方法，结合了几种旨在减少必须考虑的符号化数量的技术认证和保密属性是以一种非常自然的方式指定的，只要发现错误，就会给出攻击协议的入侵者。MIHDAMIHDA工具包[10]执行历史依赖（HD）自动机的状态最小化HD自动机由状态和标记转换组成;它们的特殊性在于状态和转换配备了名称，这些名称不再作为标签的语法组件处理，而是成为操作模型的显式部分。这允许显式地对名称创建/释放和名称挤出进行建模：这些是名称传递演算的独特机制。MIHDA已被用于执行π演算规范的有限状态验证。STASTA（Symbolic Trace Analyzer）[2]实现了密码协议的符号执行成功的攻击以违反指定属性的执行跟踪的形式报告16M. Baldamus等人/理论计算机科学电子笔记105（2004）113PWeb目录服务PWeb实现被设想为支持对π演算的某些方言中指定的系统行为的推理。它支持多种验证技术（例如，标准互模拟检查和密码协议的符号技术）的动态集成。PWeb的设计目标也是扩展可用的验证环境（移动性验证[16]，HAL [9]），并提供新的功能作为Web服务。这使我们有机会验证Web服务方法在处理“现有”模块的重用和集成方面的有效性PWeb的核心是目录服务。PWeb目录服务是一个组件，它将Web服务的描述映射到相应的网络地址。此外，它支持服务的绑定。PWeb目录维护对它使用的工具包的引用。通过WSDL规范，每个工具包在目录服务中都有一个端点。正如预期的那样，WSDL规范描述了工具包的交互功能;即哪些方法可用，以及它们的输入和输出的类型。换句话说，WSDL规范描述了服务可以做什么，如何调用它以及支持的XML类型（更准确地说是XML Schema定义XSD）。例如，MIHDA的WSDL规范提供了reduce服务的描述的reduce服务的描述是指HD的XML描述。描述π演算代理行为的自动机。在给定的HD自动机上调用此服务执行HD自动机的状态最小化。MIHDA工具包的WSDL描述如图1所示。请注意，没有什么可以阻止多个目录服务连接到相同的工具包，或者包含对其他目录服务的引用因此，PWeb基本上是一个对等系统。PWeb目录服务有两个主要设施。调用发布功能以使工具箱作为Web服务可用相反，查询工具用于发现哪些服务可用。该查询提供了服务发现机制：它会生成与参数匹配的服务列表（即，描述我们感兴趣的服务类型的XSD类型）。服务发现机制由交易引擎利用。交易引擎操纵分布在多个PWeb定向服务上的服务池。它可用于获取特定类型的Web服务并将其绑定到应用程序中。交易者引擎提供给PWebM. Baldamus等人/理论计算机科学电子笔记105（2004）1117<？XML version=“1.0”encoding=“UTF-8”？><定义名称=“Mihda”目标空间=”http://jordie.di.unipi.it:8080/pweb/Mihda.wsdl“xmlns=”http://schemas.xmlso ap.o rg/ws dl/”xmlns：soap=“http：//schemas. xmlsoap.org/wsdl/soap/“xmlns：tns=”http://jordie.di.unipi.it:8080/pweb/Mihda.wsdl“xmlns：xsd=”http://www.w3.or g/2001/XM LSchema”xmlns：xsd1=”http://jordie.di.unipi.it:8080/pweb/schemas“>/xsd：schema><消息名称=“ReduceRequest”><部件名称=“内容”类型=“xsd 1：hds_over_pi”/><联系我们<消息名称=“ReduceResponse”><部件名称=“return”type=“xsd 1：hds_over_pi”/><联系我们<操作名称=“Reduce”><文档>最小化自动机/文档><输入消息=“tns：ReduceRequest”/><输出消息=“tns：ReduceResponse”/><绑定名称=“MihdaBinding”type=“tns：MihdaPortType”><操作名称=“Reduce”><联系我们

<服务名称=“Mihda”><端口绑定=“tns：MihdaBinding”name=“MihdaPort”><服务支持Fig. 1. MIHDA WSDL规范目录服务在运行时查找和绑定Web服务的能力，而无需换句话说，Trader引擎为PWeb目录服务提供了资源发现机制。下面的代码描述了PWeb目录的一个简单的trader的实现进口商18M. Baldamus等人/理论计算机科学电子笔记105（2004）11offers= Trader.query（“reducer”）mihda =offers[ 0]#选择第一个报价=Trader.query（“模型检查”）hal = find_neighbor（offers）#仅在邻居中选择服务offers = Trader.query（“bisimulation-checking”）[0]#选择第一个交易者引擎允许在服务协调代码中隐藏网络细节。另一个好处是可以复制服务并在协调下保持对Web服务的标准访问模式。例如，代码offers= Trader.query（“安全检查器”）可用于获得编排代码，该编排代码在运行时能够查找、绑定并最终调用注册为“安全检查器”的任何服务。在PWeb原型实现中，TRUST和STA都注册为安全检查器。PWeb目录服务是使用Zope构建的[19]。Zope是一个用于构建Web应用程序的（开源）框架，旨在允许管理员以最少的工作量构建复杂且易于维护的Web服务器。通过使用数据库支持动态内容，而数据库又可以通过网络界面进行更新。Zope也是高度可配置和完全面向对象的。如果需要，可以添加和继承新对象，从而允许根据用户需要定制现有功能。还有一个强大的安全系统，允许管理员管理用户权限。Zope的一个主要优点是它是可移植的。它运行在各种机器基础架构上，包括Windows2000/NT/XP、Linux、Solaris和Max OS X。最后，我们要指出的是，trader引擎提供了与CORBA trader类似的功能。CORBA trader用于查询特定应用程序和组件的对象基础设施。PWeb 目 录 服 务 的 当 前 原 型 实 现 可 以 在 URLhttp://jordie.di.unipi.it:8080/pweb。3.1查询XML类型PWeb目录服务包括一个XML类型的数据库，该数据库跟踪可用作消息参数的XSD类型之间的关系。每当一个新的XSD类型被添加到PWeb目录服务时（例如，作为服务注册的结果），它将与现有的XSD类型及其与其他注册类型的关系M. Baldamus等人/理论计算机科学电子笔记105（2004）1119都存储在数据库中。每当应用程序执行查询时，交易引擎将提供与查询类型兼容的类型列表。在原型实现中，这是通过用Python编写的简单脚本代码获得的。我们目前正在研究用于查询XML类型的更有表现力和更强大的机制。特别是，我们开始了一些使用专门设计用于操作和查询XML数据的编程语言的实验[11，5]。4经验教训我们开始我们的实验的目的是了解是否可以有效地利用Web服务隐喻集成在一个分布式和协调的时尚基于语义的验证工具包。在这方面，PWeb的原型实现是一个很有意义的例子。我们的方法采用了一种服务编排模型，其主要优势在于通过服务目录和交易引擎的明确概念来减少网络依赖性和Web服务动态添加/删除的影响。据我们所知，这是第一个专门解决利用Web服务问题的验证环境。然而，本文提出的服务编排机制有一些缺点。特别是，它们没有充分利用SOAP的表达能力来处理类型和签名。例如，所谓的确认我们要感谢两位匿名推荐人的许多评论和建议。引用[1] A.雷苏什河Bouali，V. Roy，and R. 德·西蒙 fc2tools设置。 在CAV，卷1102的讲义在计算机科学。Springer-Verlag，1996.[2] M. Boreale和M.布西米STA，一个分析密码协议的工具（在线版本）。 Di p artimetodiS istemiedInformatica ， Universit`adiFirenze ， andDipartimentodInformatica ，Universit`adiPisa，，http：//www. 德西岛unifi.it/b或eale/tool。html，2002年。20M. Baldamus等人/理论计算机科学电子笔记105（2004）11[3] D.盒子，D.Ehnebuske， G.Kakivaya， A.外行，M.门德尔松，H. 尼尔森，S. 好的， 和D. 温纳简单对象访问协议（SOAP）1.1.WRC Note，http：//www.w3.org/TR/2000/NOTE-SOAP-2000058/，2000.[4] Volker Braun，Jurgen Kreileder，Tiziana Margaria，and Bernhard Ste Einstein. eti在线服务在行动。在TACAS，计算机科学讲义第1579卷，第439-443页。Springer-Verlag，1999.[5] 卢卡·卡德利和乔治·盖利Tql：一种基于环境逻辑的半结构化数据查询语言。出现在计算机科学中的数学结构，2003年。[6] R. Chinnici，M. Gudgina，J. Moreau，and S.维拉瓦拉那Web服务描述语言（wsdl），1.2版。技术报告，2002年。[7] 约阿希姆？兰斯？克里夫兰 帕罗， 和伯恩哈德·斯特鲁恩 并发验证：一个基于语义的并发系统验证工具。ACM Transactions on Programming Languages and Systems，15（1）：36[8] T. Web服务的业务流程执行语言（bpel4ws），1.1版。技术报告，2003年。[9] G. Ferrari，S. Gnesi，Ugo Montanari，and Marco Pistore.移动进程的模型检查验证环境。发表于ACM TOSEM，2003年。[10] Gianluigi Ferrari，Ugo Montanari，Roberto Raggi，and Emilio Tuosto.从共代数规范到实现：mihda工具包。在第一届国际组件和对象方法研讨会（FMCO），计算机科学讲义，第428-440页。Springer-Verlag，2003.[11] Haruo Hosoya和Benjamin C.皮尔斯Xduce：一种类型化的XML处理语言。ACM Transactionson Internet Technology 3（2），pages 117[12] 斯塔尔·M Web服务：超越基于组件的计算。Communications of ACM，55（10）：71[13] R. Milner，J. Parrow，and D.沃克移动过程的微积分，第一部分和第二部分。 信息与计算，100：1[14] V.VanackereTRUST 协 议 分 析 器 实 验 室 马 赛 信 息 ， http://www.cmi.univ-mrs.fr/vvvanacke/trust.html，2002年。[15] 诉范纳克尔信任协议分析器，密码协议的自动和有效验证2002年在验证研讨会-验证02[16] 比约恩·维克托和法隆·莫勒。 对于π -计算器，M b i i ityW或kbenc-atol。在DavidDill，编辑，CAVSpringer-Verlag，1994.[17] 福格尔斯W. Web服务不是分布式对象。IEEE Internet Computing，7（6）：59-66，2003.[18] W3C。技术白皮书。技术报告，2000年。[19] Zope，http://www.zope.org.