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

基于BMC的Web服务失配检测方法研究

作 者: 陈圣标
导 师: 张广泉
学 校: 苏州大学
专 业: 计算机软件与理论
关键词: Web服务 失配检测 限界模型检测 NuSMV SMT
分类号: TP311.52
类 型: 硕士论文
年 份: 2011年
下 载: 2次
引 用: 0次
阅 读: 论文下载
 

内容摘要


面向服务的体系结构(SOA)作为一种新的软件开发范型,正逐步成为未来软件发展的趋势之一,而其主流的实现方式Web服务技术也得到了快速的发展与应用。由于单个Web服务提供的功能有限,有必要将多个服务组装成一个价值增值的、粒度更大的服务或系统以满足复杂的应用需求。但在服务组合过程中,因存在接口类型、数据格式或交互协议不一致等失配情况,导致服务无法正确组合。服务失配检测可准确捕捉失配点,为实现服务的正确组合奠定基础。从互操作性分层的角度分析,服务失配可能发生在签名、行为、语义等层次。其中行为层的失配研究是关键也是难点,本文研究Web服务在行为层次的失配。如果参与交互的服务最终能到达各自的终止状态,则服务交互过程不存在失配,否则就存在失配。换言之,本文将服务的失配检测问题转化为服务兼容性判定问题。形式化验证技术(如模型检测)作为软件质量保证的一种重要方法,目前已广泛应用于Web服务相关性质验证。限界模型检测(BMC)采用由局部到全局渐进式检测,能快速寻找到反例。本文采用BMC围绕Web服务失配检测展开了研究,具体内容包括:(1)提出了一种基于NuSMV的Web服务失配检测方法。首先给出Web服务交互行为以及兼容性质的形式化描述,然后利用支持BMC的模型检测工具NuSMV验证服务交互模型是否满足兼容性质,性质不满足时,给出反例说明。(2)提出了一种基于SMT的Web服务失配检测方法,通过检测服务交互过程死锁状态是否可达来判定Web服务交互行为的兼容性。首先对Web服务交互行为进行建模,然后将其转化为SMT工具可识别的逻辑公式,并用逻辑公式表示兼容性质的否定,利用SMT工具实现Web服务的失配检测。(3)将时间属性引入Web服务交互过程中,建立带有时间属性的Web服务形式化模型,提出基于SMT的时间感知Web服务失配检测方法。

全文目录


中文摘要  4-5
Abstract  5-10
第一章 绪论  10-14
  1.1 研究背景与意义  10-12
  1.2 研究内容  12-13
  1.3 本文组织结构  13-14
第二章 Web 服务失配检测概述  14-21
  2.1 Web 服务概述  14-16
  2.2 国内外研究现状  16-17
  2.3 几种服务失配类型  17-20
  2.4 本章小结  20-21
第三章 模型检测概述  21-28
  3.1 模型检测概念  21-22
  3.2 线性时序逻辑语法和语义  22-23
  3.3 限界模型检测  23-27
  3.4 本章小结  27-28
第四章 基于NuSMV 的Web 服务失配检测方法  28-35
  4.1 Web 服务形式化模型  28
  4.2 一种基于NuSMV 的Web 服务失配检测方法  28-30
    4.2.1 NuSMV 概述  28-29
    4.2.2 Web 服务兼容性质描述  29-30
    4.2.3 基于NuSMV 的Web 服务失配检测过程  30
  4.3 实例分析  30-34
    4.3.1 构建模型  30-32
    4.3.2 代码实现  32-33
    4.3.3 实验结果  33-34
  4.4 本章小结  34-35
第五章 基于SMT 的Web 服务失配检测方法  35-45
  5.1 可满足性模理论SMT  35-36
  5.2 Web 服务并发组合  36-37
  5.3 一种基于SMT 的Web 服务失配检测方法  37-40
    5.3.1 Web 服务模型的迁移关系至逻辑公式的转换  37-39
    5.3.2 Web 服务兼容性质至逻辑公式的转换  39
    5.3.3 逻辑公式的可满足性判定  39-40
  5.4 实例分析  40-44
    5.4.1 股票分析系统模型的迁移关系至逻辑公式的转换  41-42
    5.4.2 服务兼容性质的逻辑公式表示  42-43
    5.4.3 实验结果  43-44
  5.5 本章小结  44-45
第六章 基于SMT 的时间感知Web 服务失配检测方法  45-57
  6.1 问题描述  45-46
  6.2 具有时间属性的Web 服务形式化模型  46-48
  6.3 一种基于SMT 的时间感知Web 服务失配检测方法  48-51
    6.3.1 TWSM 模型的迁移关系至逻辑公式的转换  48-50
    6.3.2 Web 服务兼容性质至逻辑公式的转换  50-51
    6.3.3 具有时间属性的逻辑公式的可满足性判定  51
  6.4 实例分析  51-56
    6.4.1 旅行订票系统模型的迁移关系至逻辑公式的转换  52-54
    6.4.2 服务兼容性质至逻辑公式的转换  54
    6.4.3 逻辑公式的可满足性判定  54-56
  6.5 本章小结  56-57
第七章 总结与展望  57-59
  7.1 本文工作总结  57-58
  7.2 未来工作展望  58-59
参考文献  59-64
攻读硕士学位期间参加的科研项目和发表(录用)的论文  64-65
附录1 股票分析系统的逻辑公式描述  65-67
附录2 旅行订票系统的逻辑公式描述  67-70
致谢  70-71

相似论文

  1. 基于用户兴趣特征的图像检索研究与实现,TP391.41
  2. 面向业务过程的服务动态组合方法研究,TP393.09
  3. 基于SOA与工作流的OA系统的研究与实现,TP311.52
  4. 基于语义的Web服务发现研究,TP393.09
  5. 行政审批电子监察系统数据交换的设计与实现,TP311.52
  6. 嵌入式网络视频应用技术的研究与实现,TP368.1
  7. 一个试卷生成系统的设计与实现,TP311.52
  8. 公安信息系统中数据集成的,TP311.52
  9. 基于Web服务的Legacy System集成方法研究,TP393.09
  10. 基于Web服务的多平台实时票务系统的研究与实现,TP393.09
  11. 基于wifi的嵌入式视频监控系统设计,TP277
  12. 水土保持自动监测信息系统研究与实现,TP311.52
  13. 基于PLSA语义聚类的web服务发现方法,TP393.09
  14. 基于QoS感知的Web服务组合,TP393.09
  15. 基于嵌入式Web服务器的便携式卫星通信地球站监控系统的设计与实现,TN927.2
  16. 一种基于用户偏好的服务组合可信模型的研究,TP393.09
  17. 基于B/S模式与OPC技术的生产线远程控制设计与实现,TP311.52
  18. 面向异构资源集成的虚拟实验平台研究,TP393.09
  19. 基于语义的Web服务匹配研究,TP393.09
  20. 基于随机Petri网的BPEL服务组合分析方法的研究,TP393.09

中图分类: > 工业技术 > 自动化技术、计算机技术 > 计算技术、计算机技术 > 计算机软件 > 程序设计、软件工程 > 软件工程 > 软件开发
© 2012 www.xueweilunwen.com