学位论文 > 优秀研究生学位论文题录展示

基于XYZ/ADL的Web服务组合验证研究

作　者: 何亚丽
导　师: 张广泉
学　校: 苏州大学
专　业: 计算机软件与理论
关键词: Web服务组合 XYZ/ADL XYZ/RE 时间自动机 精化检验 模型检测
分类号: TP393.09
类　型: 硕士论文
年　份: 2010年
下　载: 54次
引　用: 0次
阅　读: 论文下载
 

内容摘要


随着互联网和电子商务技术的发展,Web服务因其能解决Internet异构平台下服务的交互重用等问题引起了广泛关注。和传统的分布式计算模型相比,Web服务抽象程度更高、粒度更大、独立性更强,但是单一的Web服务功能有限,难以满足不断变化的业务需求,因此有必要对多个Web服务进行组合以提供更强大的功能。由于Web服务组合常用于描述跨平台跨组织的高层业务逻辑,因此保证其正确性就显得更为重要。Web服务组合是Web服务领域的研究热点,目前虽然有多种正确性验证方法,但从体系结构方面验证Web服务组合,则是一个新的研究方向。精化检验和模型检测是两种重要的形式验证技术,本文把两者应用到Web服务领域验证Web服务组合的正确性。基于上述思想,本文在课题组已有工作基础上,研究基于形式化方法和软件体系结构描述语言XYZ/ADL的Web服务组合验证问题。XYZ/ADL是时序逻辑语言XYZ/E的扩展,对有时间约束的系统而言,可由XYZ/E的实时扩展语言即XYZ/RE表示系统应满足的时间约束。考虑到多数Web服务具有实时特征,本文分析XYZ/RE和时间自动机组成元素的相似性,改进XYZ/RE到时间自动机的映射规则。针对Web服务组合系统,分别用XYZ/ADL描述其行为和性质,再将其中的XYZ/RE分别转换为对应的行为时间自动机和性质时间自动机,通过精化检验的方法判断Web服务组合系统的行为是否符合性质需求。另一方面,将单个Web服务XYZ/ADL描述中的XYZ/RE映射至单个时间自动机,多个Web服务组合XYZ/ADL描述中的XYZ/RE映射至时间自动机网络,组合后系统应满足的性质由CTL公式表示,将两者作为模型检测工具UPPAAL的输入,从而实现Web服务组合系统的正确性验证;最后分别通过网上旅游订票服务系统实例和股票分析服务系统实例说明了上述方法的可行性。

全文目录


中文摘要  4-5
Abstract  5-7
图表索引  7-11
第一章 绪论  11-16
  1.1 研究背景及意义  11-12
  1.2 国内外研究现状  12-14
  1.3 本文研究内容  14-15
  1.4 本文组织结构  15-16
第二章 形式验证技术概述  16-26
  2.1 精化检验  16-17
  2.2 模型检测  17-25
    2.2.1 标号算法  19-22
    2.2.2 不动点算法  22-24
    2.2.3 模型检测工具  24-25
  2.3 本章小结  25-26
第三章 基于XYZ/ADL 的Web 服务组合描述  26-45
  3.1 Web 服务与Web 服务组合概述  26-31
    3.1.1 Web 服务  26-29
    3.1.2 Web 服务组合  29-31
  3.2 软件体系结构描述语言XYZ/ADL 简介  31-39
    3.2.1 软件体系结构概述  31-34
    3.2.2 软件体系结构描述语言XYZ/ADL  34-39
  3.3 原子Web 服务的XYZ/ADL 描述  39-41
  3.4 Web 服务组合的XYZ/ADL 描述  41-44
  3.5 本章小结  44-45
第四章 基于XYZ/ADL 的Web 服务组合验证  45-58
  4.1 时间自动机概述  45-48
    4.1.1 时间自动机  45-47
    4.1.2 时间自动机网络  47-48
  4.2 XYZ/RE 到时间自动机的映射  48-51
  4.3 基于XYZ/ADL 的Web 服务组合精化检验  51-53
  4.4 基于XYZ/ADL 的Web 服务组合模型检测  53-56
    4.4.1 模型检测工具UPPAAL 简介  53-55
    4.4.2 Web 服务组合模型检测  55-56
  4.5 精化检验和模型检测比较分析  56-57
  4.6 本章小结  57-58
第五章 实例分析  58-63
  5.1 基于网上旅游购票服务系统的精化检验  58-60
  5.2 基于股票分析服务系统的模型检测  60-62
  5.3 本章小结  62-63
第六章 总结与展望  63-65
  6.1 本文工作总结  63-64
  6.2 进一步展望  64-65
参考文献  65-70
攻读硕士学位期间参加的科研项目和发表(录用)的论文  70-71
致谢  71-72

相似论文

  1. 基于BMC的Web服务失配检测方法研究,TP311.52
  2. 基于四方的安全电子商务支付协议研究,TP393.08
  3. 基于QoS感知的Web服务组合,TP393.09
  4. 基于本体的可信Web服务组合研究,TP393.09
  5. 基于Petri网的Web服务组合研究,TP393.09
  6. 基于随机Petri网的BPEL服务组合分析方法的研究,TP393.09
  7. 基于Agent的校友管理信息系统的设计与实现,TP311.52
  8. 基于时间自动机模型的CBTC系统安全计算机平台的形式化验证,U284.48
  9. 安全协议自动化分析系统的设计与实现,TP393.08
  10. 基于QoS的动态Web服务组合系统的设计与实现,TP393.09
  11. Web服务事务协调协议WS-TX的形式化分析与验证,TP393.09
  12. 面向生物信息领域的Web服务组合技术研究,TP393.09
  13. 基于UPPAAL的电子商务协议安全性分析,TP393.08
  14. Web服务组合容错方法研究,TP393.09
  15. 基于时间自动机的模型验证技术,TP301.1
  16. 基于MDE的UML模型到形式化模型的转换方法研究,TP311.52
  17. 基于模型检测方法的可信软件验证技术研究,TP311.52
  18. 面向环境演算系统的模型检测算法的研究,TP274
  19. 网络安全协议的模型检测分析及验证系统,TP393.08
  20. 基于OWL-S和HTN的语义Web服务组合技术研究,TP393.09
  21. 支持BQWSSM的服务组织视图的研究与应用,TP393.09

中图分类: > 工业技术 > 自动化技术、计算机技术 > 计算技术、计算机技术 > 计算机的应用 > 计算机网络 > 一般性问题 > 计算机网络应用程序
© 2012 www.xueweilunwen.com