时间约束条件下web服务组合的形式化分析与验证

摘要

随着Web技术和商业应用的快速发展，面向服务的计算(SOC)和面向服务的体系结构(SOA)也已成为人们关注的焦点。由于两者的出现，有效解决在分布以及异构环境下软件集成与复用。当前，日益成熟的Web服务技术也为两者提供了有效地技术支撑。Web服务是一种基于网络的具有松耦合、独立性强等特点的软件构件。服务是Web体系中交互的基本单位。由于单个Web服务的功能有限，web服务组合技术已成构建电子商务应用的主要方法之一。然而，如何确保在复杂环境下的Web服务能够保证软件的质量，满足人们的预期呢？特别是限定服务的行为必须满足给定的时间约束条件。形式化技术作为软件质量保证的一种重要方法。
　　本研究为适应快速变化的商业环境，对商业应用提出了实时性的要求。提出了一种形式化方法，用于分析与验证web服务组合的时间约束行为。首先，扩展了Web服务接口描述语言，增加对时间约束的描述，然后定义一种时间行为自动机，用于刻画web服务组合的时间行为，最终利用模型验证技术来自动验证这些行为是否满足给定的时间属性。通过对股票分析应用场景以及使用UPPAAL模型验证工具，表明该方法的可行性和有效性。深入研究服务组合建模与验证技术可以保障服务组合的可靠性。

目录

封面

声明

中文摘要

英文摘要

目录

主要符号对照表

第1章 绪论

1.1 研究背景及意义

1.2 研究现状

1.3 本文研究内容

1.4 本文组织结构

第2章 Web 服务组合技术概述

2.1面向服务体系架构SOA 和Web服务

2.2 Web 服务组合

2.3 本章小结

第3章 形式化技术概述

3.1 形式化方法

3.2 模型检测技术

3.3 本章小结

第4章 时间约束下Web 服务组合形式化建模

4.1 问题描述

4.2时间感知的 Web 服务组合形式化模型

4.3 实例分析

4.4 本章小结

第5章 时间约束下的 Web 服务组合分析与验证

5.1研究框架

5.2 Web服务组合模型检测

5.3 实例分析

5.4 本章小结

第6章 总结与展望

6.1 本文工作总结

6.2 未来工作展望

参考文献

致谢

个人简历、在学期间发表的学术论文