摘要由于路径可行性分析关系到测试用例的生成，因此它是BPEL程序测试中一个重要的问题。但是，由于BPEL程序支持并发和死路径消除（dead path elimination，DPE），导致现有的技术不能直接应用于BPEL程序路径可行性分析。死路径消除在BPEL流程中扩大某个不可执行活动的范围以至在该活动执行完成之后执行的所有活动都将无法完成的技术。然而，这无疑将给路径可行性分析带来巨大的困难。为了解决这个问题，我们提出一种新的方法。首先，我们将BPEL程序转化成中间模型，即BPEL控制流图（BCFG）。就DPE语义而论，控制流图是从WS-BPEL程序中抽象出的可执行流。基于BCFG这个抽象的模型，我们生成一个BPEL控制流图的逻辑表达式。该逻辑表达式能准确地表达过程变量和执行路径之间的关系，然后通过可满足性模理论(Satisfiability Modulo Theory, SMT)判定路径的可行性。 最后我们通过一个实例来验证我们这种方法的可行性和可适用性。试验的结果证明，就BPEL路径可行性分析而言，我们提出的方法比现有的方法表现得都要好。64202

毕业论文关键词：BPEL程序，路径可行性分析，死路径消除，BPEL控制流图，SMT求解器

毕业设计说明书（论文）外文摘要

Title         Static Path Feasibility Analysis for BPEL process   under Dead Path Elimination Semantics

Abstract The analysis of path feasibility is a basis and an important problem of BPEL process testing, as it relates to the test case generation. However, existing techniques cannot be directly applied to BPEL process, since BPEL process supports both parallelism and dead path elimination (DPE). DPE is a technique used in BPEL process to propagate activity disablement down paths that can no longer be executed, which brings enormous difficult for the analysis of path feasibility. To address this problem, we propose a novel approach to analyze the path feasibility of BPEL process. Firstly, we transform BPEL process into an intermediary model, BPEL control flow graph, which is proposed to abstract the execution flow of WS-BPEL process considering of the DPE semantics. Then, based on this, we produce a logical representation of BPEL control flow graph. This logical representation captures the relations between process variables and execution paths that allow path feasibility to be verified using Satisfiability Modulo Theory (SMT) solvers. We illustrate the applicability and feasibility of our approach through an application. The experimental results demonstrate that our approach outperforms existing approaches to the analysis of path feasibility in terms of BPEL process. 

Keywords  BPEL process; Path Feasibility analysis; Dead path elimination; BPEL control flow graph; SMT solver

1绪论 1

1.1研究背景 1

1.2 论文的主要工作 2

1.3论文的组织结构 2

2相关知识 。 3

2.1 软件服务 。 3

2.2 软件服务组合规范BPEL简介 4

2.3 死路径消除 6

2.4 并发静态单赋值 7

3 BPEL路径可行性分析。 8

3.1 BPEL控制流图。 8

3.2 路径可行性分析 。 12

4 案例分析 15

4.1 原型工具实现 15

4.2 试验 16

5相关工作 19

6总结与展望。 20

致谢  21

参考文献 22

图2.1  web服务基本架构 。 4

图2.2  死路径消除语义示例  7

图3.1  静态分析方法的框架  8

图3.2  块结构示意图 。 9

图3.3  建模算法   10

图3.4  情形1: 单连接   。 11

图3.5  情形2: 两个相连的<link>  。 12

图3.6  情形3: 一个<link>有两个后继<link>   12