Web服务组合形式化验证方法的研究

声明

第1 章 绪论

1.1 研究的背景和意义

1.2 国内外研究现状

1.3 本文研究的内容和结构

第2 章 Web服务组合与业务流程执行语言

2.1 Web 服务

2.2 Web 服务组合

2.3 业务流程执行语言

2.3.1 BPEL 基本活动

2.3.2 BPEL 结构化活动

2.4 本章小结

第3 章 符号模型检测与Petri 网

3.1 符号模型检测及NuSMV

3.1.1符号模型检测

3.1.2 NuSMV

3.2 Petri 网

3.2.1基本概念

3.2.2 分析方法

3.3 本章小结

第4 章 基于符号模型检测的Web 服务组合验证

4.1 方法框架

4.2 Web 服务组合的形式化定义

4.3 BPEL与有限状态自动机及NuSMV程序间的转换

4.3.1 BPEL 流程转换为有限状态自动机

4.3.2有限状态自动机转换为NuSMV程序

4.4 实例分析

4.4.1旅行预订服务

4.4.2基于消息会话的有限状态自动机模型

4.4.3 NuSMV 程序

4.4.4 属性规约

4.4.5 验证结果

4.5 本章小结

第5 章 基于符号模型与Petri 网的服务组合验证

5.1 方法框架

5.2 BPEL流程与Petri 网可达标识图及NuSMV程序间的转换

5.2.1 BPEL 流程转换为Petri 网

5.2.2 可达标识图转换为NuSMV 程序

5.3 实例分析

5.3.1可达标识图

5.3.2 NuSMV 程序

5.3.3 属性规约

5.3.4 验证结果

5.4 本章小结

总结与展望

致谢

参考文献

攻读硕士学位期间发表的论文及参与的科研工作