面向对象应用程序的模型检查行为规范

理论计算机科学电子笔记151（2006）89-105www.elsevier.com/locate/entcs面向对象应用程序的模型检查行为规范中岛申1国家信息学SORST/日本科学技术厅日本东京摘要为了提供一个框架来灵活地组合大量的专业服务，提出了一种描述Web服务流的方法。由于Web服务流程描述基本上是分布式的，因此用XML编写正确的程序并不容易。在其执行之前，审查程序是必不可少的。本文提出了一种利用SPIN模型检查器从应用程序中提取行为规范并对其进行分析的方法通过适当的抽象方法和对DPE的支持，该方法可以分析标准文档中的所有四个实例。关键词：XML，模型检查，SPIN，抽象，DPE。1引言面向服务的计算[15]是一种新兴的软件技术，用于使用Web技术的业务网络。业务合作伙伴，每个都扮演Web服务提供商的角色，相互协作，让客户从中受益。作为一个框架，组合多个Web服务，语言，如WSFL，XLANG，和BPEL 4WS的建议。BPEL4WS（Web服务业务流程执行语言），简称BPEL，旨在取代WSFL和XLANG。本文研究了OASIS标准的基础--OASIS v1.1[2]1电子邮件地址：nkjm@nii.ac.jp1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.07.03890S. Nakajima/Electronic Notes in Theoretical Computer Science 151（2006）89过程流端口调用调用接收调用答复接收调用分配调用接收由于Web流描述基本上是单个服务提供者并发执行的分布式协作，因此在Web流中编写正确的程序并发性是基于一个面向网络的工作流模型[8]，错误的行为，如死锁和违反特定于应用程序的属性，往往可以潜入的描述。在其执行之前，审查程序是必不可少的。实际上，提出了各种分析行为规范的方法[3][6][7][13][14]。本文提出了一种从可编程应用程序中提取行为规范的方法，并将其表示为扩展的可编程状态自动机（EFA）的一种变体。然后将EFA模型转换为Promela源程序，并使用SPIN模型检查器自动分析[5]。虽然在原则上可以将一个验证程序直接转换为Promela，但使用EFA作为中间表示有助于理解行为规范是什么，并以简洁的方式定义验证问题。所提出的方法进一步采用了抽象的变量上的行为的控制方面的效果，并提供了一个足够的支持DPE（死路径消除）。它可以分析所有的四个例子的情况下，在标准文件[2]。2形式化分析2.1公司简介Fig. 1.采购订单XML是WSDL（Web服务描述语言）的行为扩展。后者基本上是Web服务提供者的接口描述语言，它包含了足够的信息供客户端访问。客户机使用WSDL调用Web服务提供者。调用是一次性的; WSDL不描述提供程序的全局状态XML是一种用于表达Web服务提供者的行为组合的语言它可以通过控制和数据流链接来表达多个调用之间的因果关系Oracle采用分布式并发S. Nakajima/Electronic Notes in Theoretical Computer Science 151（2006）8991变量计算模型图1展示了一个典型的采购流程，[2]中的采购订单示例。并行计算中的并发性是基于面向网络的并发计算模型的思想，其中由流活动和控制链接（link）描述的流图表示并发性。示例程序首先等待来自外部的具有接收活动的调用请求，然后启动流中包含的三个并发活动。 在所有并发执行终止后，控制转到应答活动，该活动将某些值返回给原始外部启动器作为计算过程的结果。该示意图还使用实线（链接正如其全名所暗示的那样，XML的特点是作为Web服务架构中的业务流程描述语言，并且与工作流模式语言共享许多特性[16]。流活动的并发方面继承自WSFL，而WSFL又从PM-Graph[8]借用了其核心思想，PM-Graph[ 8]是一种工作流系统模型2.2形式分析WSDL进程与合作伙伴Web服务提供者交换消息，每个消息都确认为特定的WSDL消息类型。在纽约，tag引入消息的定义，tag定义如何操作消息数据以及如何处理控制流程，即行为规范。编译程序的正确性也有两种不同的特征：消息类型一致性和行为规范。消息类型一致性是检查交换的消息的类型是否与发送或接收消息的端口所期望的消息类型不矛盾。这个问题可以看作是类型化编程语言中的类型检查的一个变体。本文件没有进一步探讨这一问题。或者，本文侧重于系统的行为方面。这是因为行为规范在分布式并发系统中起着至关重要的作用，例如并行程序。并发系统有时可能存在潜在的死锁。 一旦系统开始执行，这种错误行为就不容易发现，因为它是不确定地发生的。系统仅在某些情况下显示出这种错误行为，并且在大多数情况下似乎正确执行。92S. Nakajima/Electronic Notes in Theoretical Computer Science 151（2006）892.3相关工作Web服务流程的形式化验证的最早工作可以追溯到S. Narayanan和S.A.Mcllraith使用Petri-net进行自动分析[13]。然而，他们不研究与Web服务标准相关的语言。针对标准技术的第一个提案是WSFL和XLANG在2001年5月宣布的。和S. Nakajima提到了一个使用模型检查技术来分析WSFL的基本思想[9][10]。尽管WSFL已经过时，但处理并发的基本技术（包括DPE）仍然适用于Windows。使用SPIN模型检查器的详细技术见[11].本文采用同样的技术来处理面向对象的数据处理过程，并研究了用模型检查器来分析面向对象的应用程序所需要的技术。抽象技术是必不可少的。目前，对可重构数据库的形式化分析大多采用基于进程代数的形式化方法。H. Foster等人使用FSP和LTSA模型检查器来建模和分析可移植程序[3]。M. 科什金娜和F. van Breugel在他们的工作中使用了CCS和并发控制（CWB-NC）[7]。G. Salaun等人还使用CWB-NC进行行为分析[14]。对于DPE，F.van Breugel和M.Koshkina [1]给出了一个有趣的分析，即执行结果可能会因是否引入DPE而不同，从而留下无意的副作用。最后，X。Fu等人通过使用抽象技术以及行为规范来处理数据方面的问题，并使用SPIN模型检查器[6]。然而，抽象技术并不总是可靠的。3行为规范3.1行为规范3.1.1基本工艺描述基本的计算元素是表示原子操作的活动。EJB提供了三种活动来与外部Web服务提供者交换信息：调用、接收和应答。invoke活动表示通过特定的合作伙伴链接调用Web服务提供者的原子操作，并等待结果。除了通信原语活动之外，为访问变量分配Activity。 它还开展其他活动，S. Nakajima/Electronic Notes in Theoretical Computer Science 151（2006）8993过程流P11P12p21P22（1）接收答复分配（2）图二. 贷款审批实现控制流程，如顺序（顺序执行）、切换（条件分支）、while（重复）和flow（并发）。XML引入了一个带有作用域活动的词法上下文。词法上下文定义了变量和各种处理程序（如异常）的有效范围。然而，考虑到确定控制流，可序列化的范围是重要的。作用域活动可以有一个serializable属性，它指定对共享资源的多个并发访问被序列化。语义与数据库事务中使用的标准隔离级别serializable非常相似[2]。它是根据严格的两阶段锁定协议定义的。3.1.2并发性流程活动引入了一个流程图，由活动本文改编了书[8]2中的语义，即基于作为工作流模式语言提出的PM-P2P模式语言。SQL的操作语义本质上是一组用于选择要触发的活动的规则图2是来自[2]LoanApproval的一个例子，使用了一个流活动和链接流有五个原子活动，它们同时执行，但具有特定于链接的接收有两个传出控制链路，每个链路都根据其他变量的值设置为true。图2使用p11和p12等变量示意性地表示条件。左侧向下的invoke（1）同样有两个链接，它们的值由p21和p22确定。两个变量是2根据与[2]作者的非正式谈话，他们的XML系统的实现已经适应了[8]中的语义。94S. Nakajima/Electronic Notes in Theoretical Computer Science 151（2006）89之所以引入这两个链接，是因为这两个链接虽然在逻辑上是相关的，但在文本中是不同的。一旦执行控制权被传递给流活动，其内部活动就同时开始执行。其中，receive可以被触发，因为它没有设置任何条件。它根据某些变量的值设置其传出链接的值。尽管图2中的条件是p11，但p11引用了下面代码片段的transitionCondition（简称tC）属性标记中的tC属性应该被适当地评估，以便进行有效的执行。示例条件涉及存储在变量request中的值，该值在接收活动中分配。由于在分析时未确定实际值，因此最好的说法是tC为真或以同样的概率失败。换句话说，链接以非确定性的方式接受任何一个值。如果将这种非确定性独立地应用于所有tC，则接收活动的两个例如，在图2中，p11和p12都为true，这在原始的JAR应用程序中并不意味着什么因此，为了正确地执行CNOW，两个传出链接应该采用不同的值。也就是说，当p11为真时，p12应为假。本文采用的方法是引入辅助谓词变量;每个条件表达式的谓词变量。然而，谓词变量的值依赖于谓词变量，因为它们构成了谓词程序中的具体表达式。对于图2中的示例，引入了两个谓词变量pred1和pred2来表示来自接收活动的两个传出链路上的条件。96S. Nakajima/Electronic Notes in Theoretical Computer Science 151（2006）89pred1pred2Δ=申请金额10000Δ=请求金额>= 10000其中，request.amount是getVariableData（'r e q u es t '，'a m o u n t '）.这两个定义具有pred2 =<$pred 1的逻辑关系此外，尽管在接收活动中分配了可变请求的值，但是在分析时不确定实际值。因此，接收活动应被视为伴随着pred1以非确定性方式取真或假另一个谓词变量pred2通过参考上述逻辑关系被适当地分配。引入谓词变量是与谓词抽象有关的一个思想[4]。本文中的方法是结构保持的。也就是说，抽象之后的描述具有与原始可编程逻辑器件程序相同的结构。4EFA建模与分析本文采用自动机理论的方法对可编程程序进行行为分析。中间表示的目的有两个：（1）定义可验证程序的行为规范是什么，（2）清楚地说明手头的验证问题。4.1使用EFA4.1.1扩展的随机状态自动机行为规范本质上是一种从控制流程的角度对系统的抽象看法然而，XML具有与数据流方面相关的语言结构：一些活动通过伙伴链接与伙伴服务提供者交换消息，并且传入消息存储在变量中。此外，变量和链接可能会影响控制流程：变量可能会出现在switch和while中的条件表达式中，也可能会在条件中使用，以触发tag中的特定链接考虑到一些变量的概念是必不可少的，全民教育将是代表性的基础形式上，EFA（扩展的状态自动机）M是一个7元组。M=Q，，V，ρ，δ，q0，FQ：位置点字母：字母包括下面的S. Nakajima/Electronic Notes in Theoretical Computer Science 151（2006）8997P！X：输出动作指示符P？X：输入操作指示符 内部动作指示符V：变量的有限集合。ρ：变量映射Q →2Vδ：跃迁关系Q × A × QA：转换动作×θ × Gθ：变量更新函数 G：保护条件q0∈ Q：初始位置F Q：Finite Set of Final Locations一个EFAM基本上是一个有限状态自动机，但有变量V，它由更新函数（θ）赋值，并用于输入/输出动作指示符（θ）和保护条件（G）的表达式中。在特定位置点的变量集合由变量映射ρ获得。转换关系δ是将源和目标位置点（Q）与转换动作A相关联的三元组。它也是一个三元组，由一个字母表（），一个变量更新函数（θ）和一个保护（G）组成。转移关系的操作意义是，当在伴随保护条件为真的条件下采取指定动作时，源的当前位置被改变为目标。变量更新函数在转换过程中执行，它为目标位置点中的指定变量分配新值。 一个变量更新函数实际上是一组变量赋值。每一个字母表中的字母可以采取三种形式之一。这两种形式，P！X和P？X与外部环境或自动机的通信有关，而X是内部动作。特别是P！X是一个输出动作指示符，而P？X是一个输入。操作上，输出动作是将值X发送到通信信道P的消息发送。输入动作是接收来自信道P的消息并且将其值设置为变量X的消息接收。最后，两个EFA4.1.2EFA for为了考虑EFA语言结构特有的功能，下面介绍了EFA的定制版本MEFA。首先，出现在输入/输出指示符中的通信通道表示连接到外部服务提供商的partnerLink其次，变量V被划分为三个不重叠的集合。V：变量的有限集合。VB+ VL+ VP VB：有限的连接变量集VL：有限的连接变量VP：Predicate Variables98S. Nakajima/Electronic Notes in Theoretical Computer Science 151（2006）89GPL：保护条件VB表示在源程序中显式出现的一组变量。它们是从<变量><过程中的标记>描述中提取的。VL是一组链接变量，每个链接<变量对应于tag of activity. <链接>用于指定<流>中并发执行活动之间的控制流，每个链接都可以被视为布尔变量。当控制流确实存在时，它被设置为true。VP是一组布尔值谓词变量，但不会显式出现在Python程序中。每个变量对应于一个谓词，该谓词表示source标记的switch、while或tC对于第3.2节中的示例，pred1和pred2是谓词变量。VL或VP中的变量都是布尔值，但VB中的布尔变量是特定于应用程序的，可以在无限域中取值。当域是无限的，或者是巨大的，如果不是无限的，在分析过程中考虑所有的潜在价值是不可行的。本文假设VB中的一个变量从一个只由定义的和未定义的两个元素组成的有限集合中取一个值。这意味着对数据空间的分析非常有限;数据值被忽略，并且数据令牌如何沿着数据流向下扩展是这里的一个问题守护条件被定制为GPL，它实际上是一个谓词，只涉及来自VL或VP的变量，不涉及来自VB的变量。保护条件表达式g要么是一个简单的布尔值表达式，要么等于（不等于）2。EFA的数据是独立的[17]。4.2核查分析技术是基于状态爆炸搜索，用于验证实际上用EFA表示的可编程程序的非线性规范为了界定核查问题，有必要作出一些定义run可以捕捉到一个非正式的概念，即一个JavaScript程序的执行过程是如何进行的。行程是EFA生成的位置点的无限序列，表示为σω=q0q1q2.其中，qi∈ Q，并且假设口吃扩展规则将有限游程表示为无限游程。接受运行也通过以下标准定义来定义：<$qf·qf∈F<$qf∈σω一个接受运行是一个成功的执行路径的EJB程序。S. Nakajima/Electronic Notes in Theoretical Computer Science 151（2006）8999第一个验证问题与可达性有关，通常被认为是对死锁自由度的检查。这是一个测试，一个可执行程序是否不会以意外的方式停止它的执行，这可以被说成是一个测试，是否有一个运行，这不是一个接受。其他有趣的属性表示在LTL（线性时序逻辑），和标准的模型检查算法可以应用。除了标准的逻辑连接词（，，<$，→）之外，LTL公式还可以有时态运算符[]（总是），<>（最终）和U并以标准的方式给出了时态运算符的运行语义。LTL公式采用一个原子命题，该原子命题是利用每个位置点的信息形成的布尔表达式。该表达式可能指的是EFA变量的值，因为EFA在其定义中有一个变量映射ρB，使得可以获得每个位置点的EFA变量。另一个感兴趣的属性是指定example经过的位置点。它可以用一个原子命题来表达询问运行是否包含为每个位置点定义的指定qi4.3EFA本节概述了从双活性到EFA片段的翻译方案。原子活动的翻译大多是直截了当的。由于EFA已经有了发送-接收通信和变量的概念，涉及与外部服务提供者通信（应答、接收和调用）和变量赋值（赋值）的活动很容易转换为适当的EFA片段。由于调用活动可以粗略地说是消息发送和接收的组合，因此EFA片段由两个连续的转换组成。形成控制序列的复杂活动可以利用EFA的保护条件。开关活动是一个多路条件分支控制，并有一个否则的分支。while活动引入了一个迭代控制，并需要一个循环结构来表示重复。流程活动的转换包括两个步骤。首先，顶流活动成为主EFA的一部分，并且直接出现在流中的每个子活动被转换为子EFA。主EFA将执行控制权转移给所有并发执行的子EFA，并等待它们的其次，所有的EFA为了同步执行，引入了控制变量。对于每个子EFA，两个布尔变量startX和endX隐式地100S. Nakajima/Electronic Notes in Theoretical Computer Science 151（2006）89引入VL。当执行控制被输入到流中时，startX被设置为真，并且因此子EFA从关于转换的保护条件变为真开始其执行。完成后，子EFA将endX变量设置为true。main确保通过使用适当的保护条件终止所有子活动。包含在流中的原子活动可以具有关于其传入链接的同步。包含的Activity具有一个特定的同步条件作为其joinCondition属性。该条件使用适当的链接变量表示为保护条件一 个 Activity 也 可 以 有 带 tC 的 标 签 。 当 tC 为 true 时 ，标记将其属性linkName设置为true，否则设置为false。这意味着linkName总是被设置为tC的值，因此可以使用变量update函数来处理。5使用SPIN5.1EFA到Promela本节介绍使用SPIN模型检查器表示EFA模型和进行分析的方法。其基本思想是将EFA转换为Promela源程序。Promela是SPIN的规范语言，它采用了一种带有变量的有限状态自动机通信的计算模型。5.1.1基本特征的翻译翻译大多是直接的，因为Promela的表达能力足以表示控制结构，通道通信和变量以及自动机。• 一个EFA自动机M变成了一个Promela过程。• 出现在输入和输出动作设计器中的通信信道P被转换为Promela信道。由于通道P表示partnerLink中，Promela通道名称的名称取自name属性。Promela通道声明考虑了交换的消息的类型channame= [0] of { mtype，short};其中mtype是描述操作（Op）的枚举类型，第二个参数携带数据值，实际上是数据标记。• 变量V在Promela中被转换为（全局）变量。具体来说，谓词变量VP是初始化为false的布尔Promela变量。S. Nakajima/Electronic Notes in Theoretical Computer Science 151（2006）89101returnfalse;链接变量VL基本上也是布尔型的，但是为了处理DPE，使用• 编码转换关系δ是翻译中最有趣的部分。控制方面直接用Promela控制语言结构编码。无条件转换由Promela序列（;）表示。EFA中的条件分支，利用保护条件G，使用Promela多路分支（如果…fi）。 重复在Promela中很容易表示，因为语言提供了循环结构（do... od）。• 输入/输出动作指示符是Promela通道操作。 P均？X和P！X被翻译成Promela对应部分。通道P被定义为如上所述的Promela通道。channelName？int n（int n）; int n（intn）;• 变量更新函数θ表示多个变量同时赋值的集合。在其Promela翻译中，原子性（atomicity {...} ）介绍。为了分析行为，Promela模型应该是封闭的。一个封闭的模型由Promela进程组成，用来模拟目标进程应该在其中执行的环境。实际上，该环境包含所有服务提供者，通过适当的合作伙伴链接与这些服务提供者进行通信。5.1.2抽象与静态分析正如3.2节所讨论的，抽象对于从一个可编程逻辑器件程序中获得一个EFA是必要的。它需要静态分析来引入适当的谓词变量（VP）。正如通过一个简单的例子简要讨论的那样，分析基本上是对控制流程有影响的变量的定义使用链（du链）此外，为每个条件表达式引入单个谓词变量。尽管图2中的示例很简单，但是接收活动的转换可能会很有趣。它需要两个逻辑相关的谓词变量。下面是与这里的讨论有关的片段=10000”/><联系我们Promela代码片段如下所示。102S. Nakajima/Electronic Notes in Theoretical Computer Science 151（2006）89客人？Request（request）;/* receive */if：：pred 1=true：：pred 1=false fi ;/* 非确定性*/pred 2=！pred 1;/* 逻辑关系 */receiveToAssess = pred1;/* source */receiveToApproval = pred2;/* source */变量pred1表示表达式request.amount 10000，它取决于变量request。pred1的d 位置在接收 活动中，在 那里它被分配了一个新值给变量request。它的u-位置在第一<个source>标记处，其中访问pred 1的值以确定链接的值。 虽然简单，但可以看出，DU链分析计算两个位置之间的正确因果关系。第二件事是确定价值。然而，最好的说法是变量pred1要么为真要么为假，因为变量request不是在分析时确定的。上面插入了代码片段，以非确定性地设置变量pred1。一旦pred1的值被分配，SPIN的模型检查方法中使用的搜索算法可以探索所有可能的值组合5.1.3DPE和可序列化作用域上面介绍了大部分的翻译，但是，对于DPE 和标记以及serializabletagtrue，应该特别注意。为了正确处理DPE，链接变量作为它的价值延伸到了强迫。强制值是在DPE启动时生成并向下显示的。如果Activity具有联接条件，则在条件的计算中，强制值将被解释为false如果Activity没有连接条件，则传入的强制值将使Activity不被执行，而是沿着Activity的传出链接进一步向下扩展。其他细节可以在其他地方找到[11]。可序列化作用域指定对作用域内变量的多个并发访问可序列化作用域应被视为构成临界区域。Promela版本为每个这样的可序列化作用域引入了一个互斥体，用于互斥访问临界区域中的变量根据标准编码风格，访问共享变量的Promela代码片段如下所示原子{ mutex== free -> mutex= busy};访问变量原子{ mutex = free}S. Nakajima/Electronic Notes in Theoretical Computer Science 151（2006）89103表1.四起案件名称产品特点国家数目(1)采购订单变量，变量249(2)航运服务切换，同时21(3)贷款审批德佩科夫3516(4)拍卖服务多个开始575.2示例情况表1给出了实验的总结。这四种情况摘自标准文件[2]。最后一列显示了使用SPIN模型检查器进行分析时的状态数。虽然它的确切值并不重要，但这个数字大致显示了分析的复杂性。如5.1节所述，翻译充分利用了Promela语言结构，在大多数示例中状态空间可以很小。第三个例子Loan Approval包含五个并发执行的活动，由于并发的交错语义，状态空间变得很大每一个例子都使用了特定的语言特征。(1)我们以采购订单（图1）作为初始示例来介绍最基本的结构和XML语言的一些基本概念。(2)Shipping Service使用switch和while活动来实现一些变量的适当由于它们的值是不确定的，抽象是必不可少的。(3)LoanApproval（图2）利用了流活动的并发性。这个例子还需要对影响转换条件的评估的变量进行抽象。(4)拍卖服务就是一个拥有多个启动活动的例子。它没有为本文的分析增加新的功能，但有趣的是，手动转换可以将状态空间的大小减小约25%。在每种情况下，一个适当的环境Promela描述介绍。环境进程是手动构造的，因此它对状态空间如第4.2节所述，LTL是一种表达某些特定于应用程序的属性的方便工具对于第三个示例Loan Approval（图2）， 可以检查是否执行了assign或invoke（2）表示如下。[]（receive→（>assign<$[]<$invoke（2）<$>invoke（2）<$[]<$assign））SPIN模型检查器确保该属性保持不变。104S. Nakajima/Electronic Notes in Theoretical Computer Science 151（2006）896讨论和结论本文报告了第一个成功的结果，可以分析文件[2]中的所有四个例子。关键点是，该方法考虑到这样有趣的功能，如DPE和控制变量的抽象。由于使用EFA作为中间表示，所提出的方法在两点上得到了清楚的理解：（1）定义了可编程程序的行为规范是什么此外，X。Fu等人[6]采用了与本文中的EFA基本相同的保护自动机模型。 两者都可以使用变量，并且转换可以具有保护条件。这种扩展的自动机对嵌入式应用程序的行为分析是一个很好的工具。其他关于对贷款审批程序进行模型检查的相关工作没有考虑DPE，也不能正确地分析贷款审批示例。另外，大多数控制变量的抽象并不重要，也没有引入谓词抽象等技术。分析结果可能比本文中的方法具有更多的假阴性这种假阴性有时是由于过度近似而忽略了对执行控制有影响的变量之间的因果关系而出现的。不幸的是，并不是所有的可编程逻辑控制器程序都可以用所提出的方法进行分析。它不处理处理程序的语义，如例外或补偿。由于处理程序是重要的语言结构，对可编程程序的行为规范有很大影响，因此在分析方法中引入这些特征是必要的。这是未来的工作之一。最后，本文所讨论的工具使用SPIN作为其后端引擎，并将结合[12]中的方法来分析嵌入式应用程序中潜在的信息泄漏。引用[1] F. van Breugel和M.科什金娜死路消除法是否有副作用？技术报告CS-2003-04，约克大学，2003年4[2] F. Curbera等，Web服务的业务流程执行语言。1.1版，2003年5月。[3] H.福斯特，S。Uchitel，J. Magee，and J. Kramer.基于模型的Web服务组合验证。InProc.ASE 2003，September 2003.[4] S. Graf和H.赛迪用PVS构造抽象状态图。在Proc. CAVS. Nakajima/Electronic Notes in Theoretical Computer Science 151（2006）89105[5] G.J. Holzmann SPIN模型 Addison-Wesley 2004.[6] X.傅氏T. Bultan和J. Su.交互式Web服务分析。在Proc. WWW 2004，第621-630页[7] M. Koshkina和F.凡·布鲁格尔。验证Web服务的业务流程技术报告CS-2003-11，约克大学，2003年10[8] F. Leymann和D.走珠精华笔生产工作流程：概念和技术。Prentice Hall 1999.[9] S.中岛Web服务流。在Proc. SAINT 2002 Workshop，第223- 224页[10] S.中岛使用模型检查技术验证Web服务流。在Proc. Cyber World 2002，第378-385页[11] S. 中岛Web服务流的模型检查（日文） 在Trans. IPS Japan，Vol.44，No.3，pages 942-952，March 2003. 2002年11月在OOPSLA 2002面向对象Web服务研讨会上提出的简明版本[12] S.中岛Web服务流中安全性和安全性方面的模型检查。InProc. ICWE[13] S. Narayanan和S.A.麦克莱斯Web服务的模拟、验证和自动组合。WWW-11，2002中。[14] G.萨劳恩湖Bordeaux和M.舍夫基于进程代数的Web服务描述与推理。InProc. ICWS[15] 作者声明：by M.P.Singh，M.N. Huhns. 面向服务的计算。Wiley 2005.[16] P. Wohed，W. van der Aalst、M.Dumas和A.特霍夫斯泰德。基于模式的BPEL 4WS分析。技术报告FIT-TR-2002-04，EUT，2002年。[17] P.沃尔珀。在命题时态逻辑中表达程序的有趣性质。在Proc. POPL