基于有色赋时Petri网的Web服务组合建模验证与测试技术研究

摘要

Web服务(Web Service)是一种自包含、自描述、模块化的应用程序，它吸收了分布式计算、网格计算和XML等各种技术的优点，解决了异构分布式计算以及代码与数据重用等问题，具有高度的互操作性、跨平台性和松耦合性，已经在电子商务、企业应用集成等领域发挥着重要作用，特别是Web服务组合技术，因其能实现服务的重用和增值而引起了世界范围内学术界和工业界的关注。
　　 Web服务组合本身是一项易于产生错误的任务，因为在组合中候选的服务之间进行复杂的交互。Web服务业务流程执行语言(Web Service Business Process Execution Language，WS-BPEL，简称BPEL)用于实现Web服务的组合和合并，它建立在IBM的Web服务流语言(Web Services Flow Language，WSFL)和Microsoft的XML业务流程语言(XML Business Process Language，XLANG)之上，结合了这两种语言的特性，这样就引起了某些方面的不一致和语义的模糊；BPEL的语义是用英语定义的，这样无法避免其二义性、模糊性和不完全性。WS-BPEL技术委员会公认为需要对BPEL语义给出形式化定义。
　　 由于要处理并发，具有复杂特性，如补偿处理、相关性、死路径删除(Dead-Path-Elimination，DPE)等，BPEL过程是容易出错的。
　　 本文主要研究由BPEL生成的Web服务组合流程的建模、验证、测试问题。
　　 针对BPEL流程建模，目前采用的方法有Petri网、SPIN工具、进程代数、抽象状态机和自动机等方法。本文采用赋时有色Petri网对BPEL流程建模。首先对BPEL的各种活动建模，将BPEL流程看作是活动的嵌套，将嵌套关系对应于层次化有色Petri网的层次关系缓解了有色Petri网模型过于庞大以及状态爆炸问题。本文提出的层次化有色Petri网的展开算法，使层次化Petri网可以展开成等价的非层次化Petri网，能够呈现出模型的细节。本文还完善了层次化有色Petri网的定义。
　　 Web服务的形式化验证是近年来才开始进入研究领域的，但是已经获得了很多研究人员的关注。针对BPEL模型验证，本文给出了利用有色Petri网的属性对BPEL流程的基本属性进行验证，使用扩展时态逻辑ASK-CTL来描述要验证的属性，对模型的动态属性进行验证的一种方法。为了处理程序验证过程中出现的状态爆炸问题，本文还对谓词抽象技术和惰性抽象技术进行了研究，将CP-nets的状态图生成过程，以及状态图的谓词抽象过程合为一体，在状态生成过程中形成抽象状态图，从而避免了状态爆炸问题。本文将惰性抽象用于BPEL流程的安全性验证方法CEGAR中，优化了“抽象-验证-反例”中的前两个步骤，使得这个方法可以用于规模较大的程序上。
　　 Web服务为分布式计算提供了灵活的、可重用的、松散耦合的模型，BPEL是半形式化的、具有复杂特性的、易含有错误行为的语言。在Web服务发布之前对服务进行验证、测试，确认服务符合设计模型是必需的。本文针对BPEL流程的CP-nets模型，提出了模型的可执行程序单元概念，基于可执行程序单元，给出了BPEL程序的测试用例生成方法，该方法可以有效的处理BPEL的并发、DPE等特性。

目录

文摘

英文文摘

作者简介

第一章 绪论

1.1 研究背景和意义

1.2 研究现状

1.3 研究内容和章节安排

第二章 Web服务组合与BPEL

2.1 BPEL的活动介绍

2.1.1 基本活动

2.1.2 结构化活动

2.2 BPEL活动中的Flow(流程)分析

2.2.1 Flow相关的标准属性和元素

2.2.2 Link的语义

2.2.3 Flow中的活动启动

2.2.4 BPEL控制流中的死路径删除

2.3 小结

第三章 有色Petri网及BPEL活动建模

3.1 Petri网介绍

3.1.1 Petri的形式化定义

3.1.2 Petri的运行规则

3.1.3 高级Petri

3.2 有色Petri网

3.2.1 CP-nets的形式化定义

3.2.2 CP-nets的作用和工具

3.3 赋时CP-nets网

3.4 BPEL活动模型

3.4.1 模型中用到的变量声明

3.4.2 基本活动(Basic Activities)

3.4.3 结构化活动(Struct Activities)

3.4.4 Flow Activity(流活动)

3.5 模型分析

3.6 小结

第四章 层次化构建BPEL模型

4.1 层次化CP-nets的形式化定义

4.2 层次化CP-nets的等价非层次化CP-nets

4.3 BPEL服务组合的层次化CP-nets建模

4.3.1 BPEL的错误处理机制

4.3.2 具有错误处理机制的BPEL层次模型

4.3.3 BPEL服务组合的层次化建模方法

4.4.BPEL服务组合建模方法的应用

4.5 小结

第五章 Web服务组合流程的CP-nets模型验证

5.1 模型验证的基本思想

5.1.1 Kripke结构(Kripke Structure)

5.1.2 模型验证的基本思想

5.1.3 模型验证包含的活动

5.2 扩展时态逻辑ASK-CTL

5.3 服务组合流程的模型验证

5.3.1 CP-nets的一般属性vs服务组合流程的性质

5.3.2 使用ASK-CTL表示CP-nets的动态属性

5.4.小结

第六章 基于抽象的CP-nets模型安全属性验证

6.1 反例引导的抽象-细化

6.2 谓词抽象

6.2.1 谓词抽象的相关概念

6.2.2 谓词细化

6.3 CP-nets模型的谓词抽象算法

6.3.1 谓词抽象算法

6.3.2 谓词抽象算法应用实例

6.4 惰性抽象

6.4.1 惰性抽象的相关概念

6.4.2 惰性抽象算法

6.5 CP-nets模型的惰性抽象算法

6.5.1 CP-nets模型与惰性抽象的先决条件

6.5.2 CP-nets模型可达树的结点分类

6.5.3 CP-nets模型的惰性抽象算法

6.5.4 惰性抽象算法应用实例

6.6 小结

第七章 Web服务组合测试用例生成技术研究

7.1 研究背景

7.2 测试覆盖标准

7.2.1 现有的BPEL测试度量标准

7.2.2 基于CP-nets模型的BPEL并发路径测试度量标准

7.3 BPEL单元测试方法

7.3.1 基于CP-nets的BPEL模型分析

7.3.2 基于控制流的程序可执行单元生成算法

7.3.3 约束处理算法

7.3.4 无效可执行程序单元的剔除

7.3.5 可并发执行的程序单元的变量共享问题

7.3.6 测试用例生成

7.4 实例研究

7.5 小结

第八章 总结和展望

8.1 本文工作总结

8.2 未来工作展望

致谢

参考文献

攻读博士学位期间的研究成果

学术论文

参加研究的科研项目