图4.1  STP约束求解器  。 15

图4.2  水利建设保障物资申请批准流程   16

图4.3  一个典型的程序  。 17

图4.4  suppressJoinFailure被设置为false的BPEL控制流图   。 17

图4.5  suppressJoinFailure被设置为yes的BPEL控制流图   18

  表4.1  一个典型程序的比较结果  。 18

 第一章  绪论

1.1  研究背景

随着 Web Service 技术日益成熟和流行，许多企业的很多部门相应地创建了 Web Service 服务。如何在不改变这些 Web Service 正常运行的情况下，将这些 Web Service 集成起来创造出新的业务模型、业务流程成为一个比较突出的业务要求。要解决这个问题，一定要有一个新的流程语言能够将 Web Service 给串起来，这种新的业务流程语言就是BPEL。

BPEL（或称为WS-BPEL），即Web服务业务过程执行语言，是为满足基于服务的业务流程需要而制定的业界事实标准[ ]。在BPEL过程的测试中，一个重要的问题就是测试数据的生成，所谓测试数据是指引起BPEL过程沿着某条覆盖语句或者分支语句或者其他的路径执行的输入数据。然而由于缺少使路径执行的输入数据，有12.5%的路径都是不可行的[ ]。因为路径可行性分析与测试样例生成相关，因此路径可行性分析是一个重要的问题。

一个程序中不可行路径的识别是不可确定的[ ]。就目前我们所了解，仍没有一种方法能够确定一个程序中大量的不可执行路径。现有的识别不可执行路径的方法大致可分为两类：静态分析技术和动态分析技术。前者主要基于符号的执行。基于符号的执行来识别不可执行路径的方法已在[ ][ ][ ]中提出。在这些技术中，用一组约束或者公式来代表一条路径。这个公式可解当且仅当存在一个输入数据使得整个程序沿着这条路径执行。通常，我们用命题验证器或者约束求解器来测试路径的可执行性。然而，由于基于符号的执行存在的局限性，使得在处理指针、数组以及函数调用中，有些不可执行路径不会被发现。动态分析技术通常采取的策略是限制深度搜索的数量和深度，如果在限制条件的情况下目标路径搜索不到，则认为该路径不可执行。总体来说，动态技术不能精确的识别路径的可行性。动态技术由于以下原因不适用于BPEL程序的路径可行性判定[ ]：测试成本，包括使用某种服务的成本；大规模测试易导致服务中断；对某些系统的影响，如证券交易系统的每一次使用都是一次业务交易。

然而，我们通常认为，在大多数的软件产品中，大部分的表达式和断言式都是线性的 [ ]。此外，通过我们的观察得到，与断言式相关的BPEL程序分支中的变量类型都是简单的并且路径条件都很容易确定。因此，静态分析方法更适合于BPEL程序的路径可行性分析。然而，现有的传统程序语言的静态路径可行性分析方法并不适用于BPEL程序，因为BPEL程序同时支持并发路径和死路径消除（DPE）。死路径消除是指扩大某个不可执行活动的范围以至在该活动执行完成之后执行的所有活动都将无法完成。这样的手段是必需的，因为每个活动都承载着充当下一个活动是否能执行的判定条件的角色。然而，这无疑将给路径可行性分析带来巨大的困难。论文网

1.2  论文的主要工作

为了解决上述问题，我们采用了一种基于BPEL控制流图（考虑死路径消除语义）的BPEL过程路径可行性分析技术。基于BPEL控制流图这个抽象的模型，我们生成一个BPEL控制流图的逻辑表达式。该逻辑表达式能准确地表达过程变量和执行路径之间的关系，然后通过可满足性模理论(Satisfiability Modulo Theory, SMT)判定路径的可行性[ ]。可满足性模理论是一个用于解决逻辑表达式组合表示的决策理论。这些理论中包含诸如数组理论、队列理论、串理论等等[ ]。此外，一个SMT求解器也能被其他新的理论所拓展，如[ ]。为了介绍本文所提出的方法，在本论文中我们只考虑线性理论。