基于时间自动机的Web服务行为分析及模拟研究

理论计算机科学电子笔记157（2006）19-34www.elsevier.com/locate/entcs基于时间自动机GregorioDiaz2Juan-Jo s'ePard o3Mar'ıa-EmiliaCambronero4Valent 'ınValero5Fernando Cuarlane6DepartamentodeInforma'ticaUniversidad de Castilla-La ManchaEscuelaPolit'ecnicaSuperiordeAlbacete. 02071-SPAIN摘要在本文中，我们将展示如何使用形式化方法来描述和分析Web服务的行为，更具体地说，包括时间限制。然后，我们的出发点是用WSCI-WSCDL（基于XML的描述语言）编写的Web服务描述。这些描述，然后转换成时间自动机，然后，我们使用一个众所周知的工具，支持这种形式主义（UPPAAL）来模拟和分析系统的行为。 作为说明，我们采取了一个特定的案例研究，旅游预订系统。保留字：Web服务，时间自动机，形式化方法。1介绍如今，社会模式正在发生变化。由于互联网和电信的发展，我们的社会是建立在信息交流的基础上的。为1这项工作得到了CICYT项目“分布式系统的描述和评估以及多媒体系统的应用”，TIC2003 -07848-C 02 -02和UCL M p r o jec t“A plic aci o n d e M o t o d os F o r m a l es a r ollo y V e r i fic aci o n d e W e b Services”的支持2电子邮件地址：gregorio@info-ab.uclm.es3电 子 邮件地址：jpardo@info-ab.uclm.es4电子邮件地址：emicp@info-ab.uclm.es5电 子邮件地址：valentin@info-ab.uclm.es6电 子 邮件地址：fernando@info-ab.uclm.es1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.12.04220G. Diaz et al./理论计算机科学电子笔记157（2006）19例如，在欧盟，ICT（信息和通信技术）的年度支出估计超过5000亿欧元，约占国内生产总值的6%。家庭和企业的互联网接入增加了。2003年，家庭上网率为45%。企业的准入率更高，在一些国家达到所有企业的90%以上（资料来源：欧洲统计局[8]）。由于社会模式的这种变化，有必要增加对基于互联网的系统开发的研究，其目标是开发自动化点对点协作的解决方案，以提高生产力并降低运营成本。因此，在过去的几年中，出现了一些用于开发这种分布式系统的新技术和语言，例如可扩展标记语言XML [14]和一些新的Web服务框架[5，9，15]，用于描述可互操作的数据和平台中立的业务接口，从而能够开发更多的开放业务交易。Web服务是新兴的、松耦合的、基于Web的计算体系结构的关键组成部分。Web服务是一个自治的、基于标准的组件，其公共接口使用XML定义和描述[11]。其他系统可能会以其定义规定的方式与Web服务交互，使用Internet协议传递的基于XML的消息。Web服务规范在用于开发和托管应用程序的异构计算环境之间架起了一座通信桥梁。电子商务应用的未来需要能够在参与服务之间执行长期的对等协作在组织的受信任域内或跨组织的用于集成交互应用程序的Web服务架构堆栈由以下组件组成[11]：• SOAP[9]：它定义了消息的基本格式以及独立于编程语言、操作系统或平台的基本交付选项。符合SOAP的Web服务知道如何发送和接收基于SOAP的消息。• WSDL[15]：它描述了Web服务的静态接口。然后，在这里定义了端点的消息集和消息特征。数据类型由XML Schema规范定义，它支持丰富的类型定义，并允许为应用程序数据表达任何类型的XML类型要求。• Registry[5]：它使可用的Web服务可见，并允许服务请求者通过相对复杂的搜索G. Diaz et al./理论计算机科学电子笔记157（2006）1921机制 它还描述了Web服务的具体功能。• 安全层：其目标是确保交换的信息不会以可验证的方式被修改或伪造，并且各方可以被认证。• 可靠的消息传递层：它为各方之间的信息交换提供了一个可靠的层，保证了信息的传递具有一个精确的一次语义。• 上下文、协调和事务层：它定义了可互操作的机制，用于传播长期业务事务的上下文，并使各方能够通过遵循全局协议协议来满足正确性要求。• 业务流程语言层[2，3]：它通过定义其控制流程（例如条件，顺序，并行和异常执行）并规定一致管理其不可观察数据的规则来描述基于Web服务的应用程序的执行• 编排层[11]：它通过从全局角度定义各方的共同和互补的可观察行为来描述各方的协作，当满足共同商定的排序规则时，信息交换发生。Web Services Choreography规范旨在任何类型的参与方之间的可互操作协作的组成，而不管托管环境的实现所使用的支持平台或编程模型。Web服务覆盖了广泛的系统，在许多情况下，这些系统具有很强的时间约束（例如，对等协作可能有完成的时间限制）。然后，在许多Web服务描述中，这些时间方面可能变得非常重要。实际上，它们目前由Web服务体系结构中的顶级层覆盖，其中包含超时和对齐等元素。超时允许每一方固定动作发生的可用时间，而对齐是两个对等方之间的同步。因此，它成为重要的Web服务框架，以确保系统的正确性与时间约束。 例如，我们可以考虑银行未能及时收到大量电子资金转账，这可能导致巨大的财务损失。然后，越来越多的人认为，使用形式化方法，基于某种形式主义的开发方法，由于这些方法带来的增强的严格性，在开发电子商务系统时可能会有显著的好处[10]。此外，这些形式主义使我们能够与所构建的模型进行推理，分析和验证一些属性，22G. Diaz et al./理论计算机科学电子笔记157（2006）19所述系统的感兴趣的特征。其中一种形式主义是时间自动机[1]，它在实践中非常常用，并且有一些众所周知的工具支持它们，如UPPAAL [6，7，12]和KHRONOS [4]。然后，本文的目标是描述如何使用模型检查技术验证具有时间约束的Web服务。此验证过程从Web服务体系结构的顶层（业务流程语言层和编排层）开始。我们在这里使用的特定业务流程语言层是Web服务编排接口（WS-CI）[2]，我们使用的具体编排层是Web服务编排描述语言（WS-CDL）[11]。因此，起点是用WS-CDL和WS-CI编写的规范文档。然而，这些描述语言对于验证过程不是很有用。将这些描述转化为时间自动化模型，并利用UPPAAL工具对系统进行了仿真和验证。为了说明这种验证方法，我们使用一个特定的案例研究，这是一个机票预订系统，其描述包含一些时间约束。本文件的结构如下。在第2节中，我们将介绍一个案例研究，该案例研究将用于说明我们为有时间限制的Web服务的验证提出的方法。在第3节中，我们描述了WSCI-WSCDL以及如何使用它们来描述案例研究.在第4节中，我们展示了如何对案例研究进行建模，并使用UPPAAL工具来模拟和验证系统行为。最后，在第5节中给出了结论和未来的工作。2案例研究：旅游预订系统在本节中，我们将介绍我们考虑的案例研究，以说明我们的验证方法。该场景由三个参与者组成：旅行者、旅行社和航空公司预订系统，其行为如下所示：一个旅行者正在计划一次旅行。一旦他决定了他想做的具体旅行，他就通过他当地的Web服务软件（Order Trip）将其提交给旅行社旅行社根据旅行者制定的标准选择最佳行程。对于此行程的每个航段，旅行社都要求航空公司预订系统验证座位的可用性（Verify Seats Availability）。因此，旅行者可以选择接受或拒绝建议的行程，也可以决定根本不进行旅行。G. Diaz et al./理论计算机科学电子笔记157（2006）1923• 如果他拒绝了建议的行程，他可以提交修改（更改行程），并等待旅行社的新建议• 如果他决定不参加旅行，他通知旅行社（取消行程），过程结束。• 如果他决定接受建议的行程（预订机票），他将向旅行社提供他的信用卡信息，以便正确预订行程。一旦旅行者接受了建议的行程，旅行社将与航空公司预订系统连接，以便预订座位（保留座位）。然而，可能发生的是，在那个时刻，对于行程的特定段没有座位可用，因为从进行可用性检查的时刻起已经过去了一些时间。在这种情况下，航空公司预订系统会通知旅行社（无座位），旅行社会通知旅行者行程无法进行（取消通知）。预订完成后，旅行社将通知旅客（已预订座位）。然而，此预订仅在一天内有效，这意味着如果在此期间未收到最终确认，则座位未被预订，旅行社将被告知。因此，旅客现在可以确认预订或取消预订。如果他确认预订（预订机票），旅行社要求航空公司预订系统最终预订座位（预订座位）。根据前面的描述，在全局过程（称为PlanAndBookTrip）内交换的消息的高级流程如图1所示，并且更完整的描述（包括由每个参与者执行的动作）如图1所示二、3WSCI-WSCDL描述Web服务编排规范旨在能够精确地描述任何类型的参与方之间的协作，而不管托管环境的实现所使用的支持平台或编程模型。使用Web ServicesChoreography规范，生成包含对消息交换所依据的公共排序条件和约束的“全局”定义的契约，该契约从全局角度描述所有相关方的公共和互补的可观察行为。然后，各方可以使用全局定义来构建和测试符合该定义的解决方案。全局规范反过来又通过在适当的基础设施支持的基础上组合所产生的本地系统来实现。24G. Diaz et al./理论计算机科学电子笔记157（2006）19Fig. 1. 交换的消息流图二. PlanAndBookTrip的整体图片。在现实世界的场景中，公司实体通常不愿意将其业务流程的控制权委托给其集成伙伴。编舞是一种手段，通过这种手段，合作中的参与规则可以明确定义并共同商定然后，每个实体可以实现其G. Diaz et al./理论计算机科学电子笔记157（2006）1925图三. WS-CDL和WS-CI用法。由公共或全局视图确定的编排的一部分。WS-CDL的意图是，很容易确定每个实现与WS-CDL中表达的公共视图的一致性。图3显示了编排描述语言的可能用法。在我们使用的特定示例中，我们将WS-CI作为业务流程执行层（简称WS-CI）。但是，在此之前，我们必须提供WS-CDL描述。WS-CDL描述了各方之间的可互操作协作。为了促进这些合作，各部门通过建立关系来承担相互责任。他们的合作发生在一个共同商定的一套排序和约束规则，从而双方之间交换信息WS-CDL模型由以下实体组成：• 参与者类型、角色类型和关系类型：在编排中，信息总是在信任边界内或跨信任边界的各方之间交换。角色类型列举了一方为了与其他方协作而表现出的可观察行为。关系类型确定了双方成功合作所必须做出的相互承诺。参与者类型将必须由同一逻辑实体或组织实现的可观察行为的那些部分分组在一起。• 信息类型、变量和令牌：变量包含关于协作中通常可观察的对象的信息，诸如所交换的信息或所涉及的角色的可观察信息。26G. Diaz et al./理论计算机科学电子笔记157（2006）19标记是别名，可用于引用变量的各个部分。变量和令牌都有类型，定义变量包含的结构或令牌引用。•编排：它们定义了互动方之间的协作：· 编舞生命线，表达了合作的进展。最初，合作是在各方之间建立的，然后工作在其中进行，最后它正常或不正常地完成。· 编排异常块，指定当编排以异常方式运行时应发生· Choreography Finalizer Block，描述如何指定修改先前成功完成的Choreography的结果时应发生的其他交互（例如，确认或撤消等）。• 渠道：它们通过指定信息交换的地点和方式，在各方之间建立协作点• 工作单元：它们规定了必须满足的限制，以便在编排中取得进展并执行实际工作• 活动和排序结构：活动是执行实际工作的编排的最低级别排序结构将活动与嵌套结构中的其他排序结构组合，以表达在Chore-ography中交换信息的排序条件。• 交互活动：它是编排的基本构建块，其导致各方之间的信息交换以及它们的可观察信息变化和所交换信息的实际值的可能同步。• 语义：它允许创建描述，可以记录模型中每个组件的语义定义图4显示了WS-CDL文档的一部分，它描述了我们的案例研究。这部分说明了航空公司和旅行社之间的关系。我们可以看到，这个交互描述决定了一个预订可用的最大时间只有一天。3.1WSCIWSCI是一种接口描述语言。它描述了服务的可观察属性以及从外部与服务交互的规则。 它不是一种可执行语言，但它足够精确和明确。G. Diaz et al./理论计算机科学电子笔记157（2006）1927<交互名称=“预订”channelVariable=“travelAgentAirlineChannel”operation=“reservation booking”align=“true”initiate=“true”><交易所名称=“预订”informationType=“预订”action=“request”><发送变量=“tns：reservationOrderID”causeException=“true”/><接收变量=“tns：reservationAckID”causeException=“true”/><联系我们<交换name=“booking”informationType=“booking”action=“respond”><发送变量=“tns：bookingRequestID”causeException=“true”/><接收变量=“bookingAckID”causeException=“true”/><联系我们<记录名称=“bookinglist”when=“timeout”causeException=“true”/><源变量=“AL：getVariable（<目标variable=“TA：getVariable（见图4。 WS-CDL规范消息交换中的每一方的可观察行为都是独立于其他方来描述的。WSCI的基本结构是Action，它绑定到一些WS-CDL操作.WSCI语言的主要概念如下：接口：WSCI将Web服务的描述映射到接口的概念。活动和活动编排：WSCI用编排的活动来描述Web服务的编排描述活动之间的时间和逻辑依赖关系，其中原子活动表示Web服务的基本行为单元重用的过程和单元：过程是行为的一部分，标有名称。可以通过引用其名称来重用它属性：它允许我们在接口定义中引用一个值它们相当于其他语言中的变量上下文：它描述了执行一组活动的环境。每个活动都在一个上下文定义中定义28G. Diaz et al./理论计算机科学电子笔记157（2006）19消息相关性：它描述了会话是如何构造的，以及为了正确地执行服务必须交换哪些属性注：例外的定义是上下文定义的一部分。有三种异常，当异常发生时，当前上下文必须在与异常相关的活动执行后终止。交易和补偿活动。事务断言一组活动以全有或全无的方式执行。事务可以声明一组补偿活动，如果事务成功完成，则将执行这些活动，但需要撤消。全局模型：全局模型由参与服务的接口集合和操作之间的链接集合通信服务。3.2Example.旅行预订系统我们现在介绍所考虑的案例研究的建模细节3.2.1旅行社界面旅行社的模式有以下要素：• 旅行社的主要活动通过嵌套的流程表示。• 迭代过程通过while活动来描述• 我们使用异常来捕获旅行请求或预订请求的撤销。• 该接口使用两种不同的相关性，这两种相关性识别涉及旅行社与旅行者和航空公司预订系统的相同对话。图5显示了旅行代理规范的一部分，其中定义了一个处理预订超时的异常。3.2.2工艺卡界面描述Traveler的主要顶级流程使用instantia- tion=other属性声明，以描述Traveler实际上是启动消息交换的实体。请注意，该模型通过带有新异常的新上下文捕获取消预订或机票预订的可能性。我们使用相关性来确保旅行社和航空公司G. Diaz et al./理论计算机科学电子笔记157（2006）1929...<联系我们<例外><在线留言><动作名称=“ReservationTimeOut”role=“tns：TravelAgent”operation=“tns：TAtoAirline/AcceptCancellation“><相关correlation=“defs：reservationCorrelation”/><故障代码=“tns：reservationTimedOut”/><在线留言......<联系我们图五. 部分旅行社规格预订系统知道如何满足旅行者界面所展示的相关要求。3.2.3航空预订系统机票预订系统接口由一个带有两个顶级流程的接口建模，这两个流程都带有instantiation=message属性。每个航段的座位预订被定义为一个交易，该交易定义了一个补偿活动，该活动可能会撤回所有座位的预订。图6显示了规范的一部分（超时控制）。4建模、仿真和验证前面的描述可以转化为时间自动机，从而得到三个自动机，分别对应于旅行者，旅行社和航空公司。这些自动机如图7、图8和图9所示。30G. Diaz et al./理论计算机科学电子笔记157（2006）19...<联系我们<例外><联系我们<联系我们...见图6。 部分旅行社规格有空吗？no_available？ordertrip？更改行程！取消行程！开始预订机票！没有预约吗？notify_timeout？收到票了吗？没有预约吗？receive_statement？预订机票！取消预订！accept_cancel？见图7。 旅行者的时间自动机注意图8中时钟x的使用，以控制预留何时到期。这个时钟是初始化一旦预留座位完成。通过模拟，我们可以检查系统模型是否具有预期的行为。这些模拟是通过选择不同的过渡和延迟沿系统的演变。在模拟过程中的任何时刻，您都可以看到变量值和可以选择的启用的变换。因此，您可以选择要执行的转换。然而，您也可以选择随机执行转换，因此，系统通过以随机方式执行转换和延迟来进化。我们在模拟器中还有其他选择。例如，您可以保存模拟跟踪，以便以后用于恢复特定的执行跟踪。事实上，G. Diaz et al./理论计算机科学电子笔记157（2006）1931没有座位了！check_seats？available_seat！预订座位？暂停！x==24预订座位！x：=0领取门票！X 24预订座位！X 24预订座预订座位没有！X 24取消预订座位？取消预订座位！no_available！有空座位吗？检查座位！ordertrip！接受_取消！可用！没有座位了吗？改变行程？取消行程？没有预约！预订票？预订座位号？reserve_seat！暂停？预订座位好吗？通知超时！receive_语句！暂停？book-ticket？取消预订？预订座位好吗？没有预约！预订座位！预订座位号？取消预订座位好吗？取消预订座位！reserve_seat_no！图8.第八条。航空订票系统的时间自动机见图9。 旅行社的定时自动机。在这一点上，模拟是相当灵活的，你可以在序列中向后或向前。然后，我们在案例研究的验证阶段的主要目标是检查消息队列和超时的正确性，同时考虑协议定义。我们已经进行了大量的模拟，我们得出的结论是，系统设计满足了各方之间消息流的预期行为。在开始自动验证之前，我们必须确定模型必须满足哪些属性。我们将这些属性分为三类：安全性，活动性和死锁。这些属性是通过时间逻辑来指定的，并且所有这些属性都已经使用UPPAAL工具进行了检查UPPAAL使用的时态逻辑在[13]中描述。32G. Diaz et al./理论计算机科学电子笔记157（2006）19安全属性：它们允许我们检查我们的模型是否满足一些安全限制。例如，如果我们有两列火车必须通过同一座桥，安全属性是两列火车不能同时通过这座桥：Q <$（列车1.穿越¬∃♦(T rain1.crossing∧Train 2.crossing)我们案例研究的主要安全属性如下：•旅行社总是根据旅客的要求发送行程(1)QQ旅行者.行程 旅行社TravelAgent.sendItinerary• TravelAgent始终根据旅行者的要求更改行程(2)QTraveler.ChangeItinerary• TravelAgent始终根据旅行者的要求取消预订(3)Q旅行者.取消预订→（TravelAgent.CancelReservtRcv）取消预订航空公司。Clockx24）• 预订仅在执行预订前24小时提供：(4)旅行社预订服务Airline.ReceiveBoking（Airline.ClockX<= 24）• 旅行者总是在付款后收到他的机票和对账单(5)QTraveler.付款P erf（Traveler.F inishAirline.SnddTcktTravelAgent. SenddStttment）活性属性：他们打算检查我们的模型是否可以按照正确的顺序进化回到火车的例子，如果一列火车接近桥，一段时间后，火车将能够通过它：列车接近→列车交叉我们模型的活动属性很简单，例如，如果旅行者发送旅行需求，一段时间后，TravelAgent将发送行程。将其转换为时间逻辑，我们有：(6)Traveler.P lanOrder−→TravelAgent.SendItinerary另一个有趣的活性属性如下：如果旅行者命令在预订后的24小时内预订，航空公司执行预订。将其转换为时间逻辑，我们有：(7) （Traveler.BookOdrAirline.ClockX24）−→Airline.PerformBookG. Diaz et al./理论计算机科学电子笔记157（2006）1933死锁：这些是明确的限制。我们可以用下面的公式来检查我们的模型是否是无死锁的：(8)死锁5结论和今后的工作在本文中，我们已经展示了如何应用形式化方法来确保Web服务的正确性与时间限制。我们已经证明，我们可以将WSCI-WSCDL中编写的描述转换为时间自动机，因此，我们可以使用UPPAAL工具来模拟和验证系统行为。在我们用来说明这种方法如何工作的特定案例研究中（机票预订系统），这种翻译是手动进行的，但我们的目的是研究这种翻译是否可以自动进行，并在这种情况下实现支持这种翻译的工具是的。引用[1] R. Alzheimer 和 D. 迪 尔 实 时 系 统 建 模 的 自 动 机 在 Proceedings of the 17th InternationalColloquium on Automata，Languages and Programming，卷443，编辑。Springer–Verlag,[2] Assaf Arkin et al.Web Service Choreography Interface （ WSCI ） 1.0. 在 http ：/www.w3.org/TR/wsci/上。[3] Assaf Arkin，Sid Askary，Ben Bloch，et.例如，Web服务业务流程执行语言2.0版，编辑器。OASISOpen，2004年12月。见http://www.oasis-open.org/committees/download.php/10347/wsbpel-specification-draft-120204.htm。[4] M.博兹加角道斯岛Maler，A. Olivero，S. Tripakis和S.尤文Kronos：一个实时系统的模型检查工具。In Proc. 1998 Computer-Aided Verification，CAV计算机科学讲义1427，Springer-Verlag。[5] Luc Clement，Andrew Hately，Claus von Riegen和Tony Rogers。版本3.0.2，编辑器。2004年10月19日，绿洲公开赛。在http://uddi.org/pubs/uddi v3.htm中。[6] G. Diaz，F. Cuarlovan，V. Valero和F.佩拉约TLS 握手协议的自动验证。2004年ACMSymposium on Applied Computing。[7] G. Diaz，K.G. Larsen，J. Pardo，F. Cuarlovan和V. Valero。 一种处理电子商务中实时和概率行为的方法：验证SET协议。2005年ACM Symposium on Applied Computing。[8] 2004年欧统局年鉴。欧洲统计指南。1992-2002年数据。欧洲联盟委员会：欧统局，欧洲共同体官方出版物办公室，2004年[9] Marc Hadley，Noah Mendelsohn，Jean-Jacques Moreau，et. SOAP Version 1.2 Part1 ： Message Framework ， Editors. 万 维 网 联 合 会 ， 2003 年 6 月 24 日 。 在http://www.w3.org/TR/soap12-part1。[10] 康斯坦斯·海特梅尔和迪诺·曼德里奥利实时计算的形式化方法。约翰·威利父子公司一九九六年。34G. Diaz et al./理论计算机科学电子笔记157（2006）19[11] NickolasKavantzas 等 人 Web 服 务 编 排 描 述 语 言 （ WSCDL ） 1.0.在http://www.w3.org/TR/ws-cdl-10/。[12] K. Larsen和P. Pettersson和Wang Yi。你在坚果壳里。技术转让软件工具国际杂志，编辑。[13] Kim G.放大图片作者：Paul Petterson. 实时系统的诊断模型检查。混合系统的验证与控制研讨会论文集III，《计算机科学讲义》，第1066卷，页。575-586，1995年。[14] Jean Paoli，Eve Maler，Tim Bray，et. al. 可扩展标记语言（XML）1.0（第三版），编辑。万维网联盟，2004年2月4日。在http://www.w3.org/TR/2004/REC-xml-20040204。[15] Sanjiva Weerawarana ， Roberto Chinnici ， Martin Gudgin ， et. Web 服 务 描 述 语 言（ WSDL ） 2.0 版 第 1 部 分 ： 核 心 语 言 ， 编 辑 器 。 万 维 网 联 盟 ， 2004 年 8 月 3 日 。 在http://www.w3.org/TR/2004/WD-wsdl20。[16] Simon Woodman等，Specification and Verification of Composite Web Services。2004年第八届企业分布式对象计算