Web服务线性时态逻辑模型检查研究

摘要

由于应用的复杂性，在很多情况下单个Web服务难以满足实际需求，对于复杂业务过程的处理需要采用服务组合的方法即由各个小粒度的Web服务相互之间通信和协作来实现大粒度的服务功能。Web服务组合常用于描述跨组织的业务流程等高层业务逻辑，这意味着系统的任何错误都可能导致严重的损失。保证服务组合的正确性，确认服务组合的有效性是Web服务组合系统成功的关键。 本文将基于自动机的模型检查技术应用到Web服务组合中。首先从语义角度研究了PROMELA语义引擎问题。PROMELA语言是模型检查工具SPIN的核心，对PROMELA语言执行方式的理解决定所描述系统模型的行为方式。论文给出PROMELA语法的抽象对象模型的形式化定义和一个算法来实现PROMELA语法到抽象对象模型的映射，描述了PROMELA指称语义。针对SPIN中原子序列和同步通信等复杂问题给出了解决方法。 然后提出了对基于WS—CDL的Web服务组合的PROMELA建模与验证。WS—CDL支持的控制流机制包括：顺序、并发、同步、条件、非确定性选择等。论文提出了一种Web服务数据流和控制流的模型，可以在数据流和控制流之间验证不利的交互。WS—CDL进程模型的PROMELA映射关键在于WS—CDL进程模型验证相关方面的确定以及如何执行这种映射。 最后利用模型检验工具SPIN对有第三方支付平台参与的网上交易进行形式化分析。实验证明此方案能够对基于WS—CDL的Web服务组合进行行之有效的验证。

目录

文摘

英文文摘

声明

1绪论

1.1研究背景

1.2论文的研究意义

1.3国内外的研究现状

1.3.1 Web服务组合方法

1.3.2 Web服务的模型检查

1.4论文的主要研究内容

1.5论文的结构安排

2理论基础

2.1 Web服务

2.1.1 Web服务的基本概念

2.1.2 Web对象

2.1.3 Web服务不同角度的描述

2.1.4 Web服务的体系架构模型

2.2模型检查

2.2.1模型检查原理

2.2.2线性时态逻辑

2.2.3模型检查算法

2.2.4模型检查工具

2.3本章小结

3 PROMELA语义模型执行方式研究

3.1 SPIN模型检查的基本过程

3.2 PROMELA语义模型

3.3 PROMELA语句到语义模型的映射算法

3.4本章小结

4 Web服务编排的建模与分析

4.1 WS-CDL语言

4.2 WS-CDL进程模型的PROMELA建模

4.2.1复合进程建模

4.2.2分割和分割合并进程建模

4.2.3顺序结构建模

4.2.4条件选择结构建模

4.2.5原子进程建模

4.2.6数据流建模

4.2.7循环结构建模

4.3验证数据流和控制流的交互

4.4本章小结

5第三方支付的形式化建模及特性验证

5.1第三方支付的形式化建模

5.1.1第三方支付交易流程

5.1.2第三方支付的形式化建模

5.1.3第三方支付的属性描述

5.2 Amazon例子的验证

5.3本章小结

6总结和展望

参考文献

附录：攻读硕士期间发表的论文

致谢