学位论文 > 优秀研究生学位论文题录展示
基于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
|
相似论文
- 基于用户兴趣特征的图像检索研究与实现,TP391.41
- 面向业务过程的服务动态组合方法研究,TP393.09
- 基于SOA与工作流的OA系统的研究与实现,TP311.52
- 基于语义的Web服务发现研究,TP393.09
- 行政审批电子监察系统数据交换的设计与实现,TP311.52
- 嵌入式网络视频应用技术的研究与实现,TP368.1
- 一个试卷生成系统的设计与实现,TP311.52
- 公安信息系统中数据集成的,TP311.52
- 基于Web服务的Legacy System集成方法研究,TP393.09
- 基于Web服务的多平台实时票务系统的研究与实现,TP393.09
- 基于wifi的嵌入式视频监控系统设计,TP277
- 水土保持自动监测信息系统研究与实现,TP311.52
- 基于PLSA语义聚类的web服务发现方法,TP393.09
- 基于QoS感知的Web服务组合,TP393.09
- 基于嵌入式Web服务器的便携式卫星通信地球站监控系统的设计与实现,TN927.2
- 一种基于用户偏好的服务组合可信模型的研究,TP393.09
- 基于B/S模式与OPC技术的生产线远程控制设计与实现,TP311.52
- 面向异构资源集成的虚拟实验平台研究,TP393.09
- 基于语义的Web服务匹配研究,TP393.09
- 基于随机Petri网的BPEL服务组合分析方法的研究,TP393.09
中图分类: > 工业技术 > 自动化技术、计算机技术 > 计算技术、计算机技术 > 计算机软件 > 程序设计、软件工程 > 软件工程 > 软件开发
© 2012 www.xueweilunwen.com
|