Web服务作为一种面向服务架构的新型分布式计算模型,在分布式平台上发挥着越来越重要的作用。作为Web服务组合的事实标准,BPEL利用flow和link等元素实现了并发和同步机制,以提高效率;但同时也引入了常见的并发缺陷,如数据竞争、原子性违反、顺序性违反等。数据竞争是指:在并发程序中,不同线程的两个操作对相同的共享变量的访问没有特定的顺序,且其中至少有一个是写操作的情况。数据竞争是最常见的一种并发缺陷,只会在线程间特定的切换下才会发生,很难检测和定位,并且会造成死锁甚至宕机等严重后果。目前已有的数据竞争检测方法大致可以分为两种:基于Lamport提出的HB(Happens-Before)序关系的检测方法和基于锁集(lockset)的检测方法。但由于BPEL语言独有的特性(如死路径删除DPE、link等机制),使得这些方法不能直接用来检测组合Web服务中的数据竞争。为此,本文借鉴已有的检测方法并结合BPEL语言相关特性,提出了一种基于静态分析和约束求解的BPEL数据竞争检测方法SACS4BPEL和一种基于预测性分析的检测方法PA4BPEL,系统完整地提出了 BPEL程序中与并发相关的各种约束模型,包括HB序约束模型、link约束模型、锁约束模型、DPE约束模型和读写约束模型等。SACS4BPEL方法主要包括3个模块:静态分析模块、约束建模模块和约束求解模块:(1)静态分析模块:首先通过静态分析获得BPEL流程中活动与变量的“读写”关系VRW,并通过分析数据流和控制流信息给每个活动赋予一个全局标识GID;然后依据GID信息构造活动间的HB图(Happens-BeforeGraph);此外,还提取了 BPEL程序中与并发相关的一些元素信息包括link、Isolated Scope、Correlation Set 等。(2)约束建模模块:主要构造活动间的发生序约束模型,包括线程内约束模型和线程间约束模型。线程内约束主要是HB序约束,线程间约束包括link约束和锁约束。(3)约束求解模块:首先通过对约束模型进行编码,然后将SMT求解器作为求解工具来检测是否存在数据竞争。实验结果表明:SACS4BPEL可以有效的检测出BPEL程序中潜在的数据竞争,但结果中存在少量的误报FP问题。实验过程中的数据主要来源于 Oracle BPEL PM Sample和WS-BPEL Composition Repository。我们从中选取了 10 个具有代表性BPEL程序作为实验对象,这些数据基本囊括了较为常见的BPEL程序。在我们的实验数据集上,SACS4BPEL的准确率Precision可达到76.7%,明显好于现有的方法,但检测结果受程序规模变化的影响比较大。因此,本文又提出了 PA4BPEL检测方法。PA4BPEL主要包括5个模块:预处理模块、预测生成执行轨迹模块、构造执行轨迹闭包集CL(T)模块、约束建模模块和约束求解模块。PA4BPEL与SACS4BPEL的区别在于前者需要通过BPEL执行引擎执行BPEL程序而后者不需要;前者的约束条件都是在执行轨迹中分析得到而非直接从源代码中获得,而后者是基于源程序分析获得。PA4BPEL的具体实现过程包括:插桩、收集执行轨迹、预测生成执行轨迹、构造执行轨迹闭包集CL(T)、构造约束模型、约束求解等。实验结果表明PA4BPEL的检测结果中不存在误报FP问题,但存在部分漏报FN问题;原因在于预测生成执行轨迹过程中为了兼顾检测效率,没有使得轨迹覆盖率达到100%。在我们的实验数据集上,PA4BPEL的召回率Recall可达到83.8%,且检测结果受程序规模变化的影响不大。