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

Web服务事务协调协议WS-TX的形式化分析与验证

作　者: 李祥
导　师: 黄志球
学　校: 南京航空航天大学
专　业: 计算机应用技术
关键词: Web服务 事务处理 形式化方法 Pi-演算 协议建模 模型检测
分类号: TP393.09
类　型: 硕士论文
年　份: 2009年
下　载: 37次
引　用: 0次
阅　读: 论文下载
 

内容摘要


Web服务作为一种新的计算模型正受到越来越多的关注,保证Web服务组合执行结果的一致性和可靠性是Web服务面临的重要挑战之一。将事务机制应用到Web服务领域是寻求解决Web服务组合执行结果一致性和可靠性问题的重要手段。针对Web服务自治、跨组织以及长周期等特点,工业界基于传统事务机制提出了新的事务处理协议和标准。其中,Web服务事务协调协议WS-TX由于利用了现有的和正在制订的标准,能够融入Web服务架构,得到了业界的广泛关注。由于WS-TX协议采用自然语言描述,缺乏严格的语义,很多学者使用形式化方法对其进行研究,验证协议本身的正确性。然而,协议的正确并不代表使用协议的应用场景也能满足事务特性。本文采用Pi-演算对WS-TX协议应用场景进行建模,使用符号化模型检测工具NuSMV2从“安全性”和“活性”两方面对模型进行验证和分析。主要工作分为以下三个方面:1.针对WS-TX应用场景的并发特性,采用Pi-演算对其进行建模。给出了WS-TX协议应用场景与Pi-演算元素的映射关系,并在此基础上给出了建模规则。通过对应用了WS-TX中WS-AT协议的银行转帐场景和WS-BA协议的旅行安排场景的协调过程进行Pi-演算建模,验证了建模规则的可行性。2.由于现有Pi-演算模型检测工具存在检测能力不足的问题,本文将Pi-演算模型转化为SMV程序(有限状态自动机模型),利用NuSMV2进行检测。根据标号变迁系统到Kripke结构的映射关系找出Pi-演算模型到SMV程序的转换规则,并实现了自动转换工具PiCal2NuSMV.3.分析了WS-TX中两个事务协议WS-AT和WS-BA应用场景的安全性和活性,用计算树逻辑CTL进行描述,并采用NuSMV2检验银行转帐和旅行安排的业务协调过程是否满足这些性质,验证结果表明应用场景满足事务特性并且协议本身是可靠的。同时,进一步讨论和分析了NuSMV2生成的反例。

全文目录


摘要  4-5
Abstract  5-11
第一章 绪论  11-15
  1.1 课题研究背景及意义  11-12
  1.2 Web 服务事务的国内外研究现状  12-13
  1.3 本文研究内容和组织结构  13-15
第二章 Web 服务事务问题描述  15-28
  2.1 Web 服务及其相关技术  15-17
  2.2 Web 服务事务研究现状  17-19
    2.2.1 事务的概念  17-18
    2.2.2 Web 服务中的事务问题  18-19
  2.3 Web 服务事务协调协议WS-TX  19-27
    2.3.1 Web 服务协调 WS-Coordination  20-22
    2.3.2 Web 服务原子事务 WS-AtomicTransaction  22-25
    2.3.3 Web 服务业务活动 WS-BusinessActivity  25-27
  2.4 本章小结  27-28
第三章 基于Pi-演算的 WS-TX 协议应用建模  28-40
  3.1 Pi-演算建模分析  28-29
  3.2 面向WS-TX 协议应用场景的Pi-演算建模方法  29-32
    3.2.1 WS-TX 协议应用场景元素与Pi-演算元素的映射关系  29-30
    3.2.2 WS-TX 协议应用场景的Pi-演算建模规则  30-32
  3.3 WS-TX 协议应用场景建模  32-39
    3.3.1 WS-TX 协议应用场景  32-33
    3.3.2 WS-TX 协议应用场景的Pi-演算模型  33-39
  3.4 本章小结  39-40
第四章 Pi-演算模型的SMV 程序表述  40-55
  4.1 基于NuSMV2 的模型检测方法  40-41
  4.2 Pi-演算模型到SMV 程序代码的转换  41-50
    4.2.1 理论基础  42-48
    4.2.2 转换规则  48-50
  4.3 转换工具PiCa12NuSMV 的设计与实现  50-54
    4.3.1 Pi-演算文本解析器  50-52
    4.3.2 转换适配器  52-53
    4.3.3 SMV 程序产生器  53-54
  4.4 本章小结  54-55
第五章 基于NuSMV2 的 WS-TX 协议应用模型检测及分析  55-62
  5.1 WS-TX 协议应用性质分析  55-57
    5.1.1 WS-AT 应用场景的性质分析  56
    5.1.2 WS-BA 应用场景的性质分析  56-57
  5.2 基于计算树逻辑CTL 的WS-TX 应用模型的性质归约  57-59
    5.2.1 WS-AT 应用场景性质的CTL 描述  57-58
    5.2.2 WS-BA 应用场景性质的 CTL 描述  58-59
  5.3 基于 NuSMV2 的模型检测及其分析  59-61
    5.3.1 WS-AT 应用场景性质检测及分析  59
    5.3.2 WS-BA 应用场景性质检测及分析  59-60
    5.3.3 进一步思考  60-61
  5.4 本章小结  61-62
第六章 总结与展望  62-64
  6.1 论文工作总结  62-63
  6.2 进一步的工作  63-64
参考文献  64-68
致谢  68-69
在学期间的研究成果及发表的学术论文  69-70
附录  70-78
  附录1 银行转帐SMV 程序代码  70-72
  附录2 旅行安排SMV 程序代码  72-76
  附录3 飞机订票Web 服务的原子性模型检测反例  76-78

相似论文

  1. 基于用户兴趣特征的图像检索研究与实现,TP391.41
  2. 面向业务过程的服务动态组合方法研究,TP393.09
  3. 基于面向服务架构的公众信息系统在新农村信息化建设中的应用研究,TP393.09
  4. 基于嵌入式Web服务器的监控系统研究,TP393.05
  5. 一种基于领域本体的语义Web服务匹配和组合方法,TP393.09
  6. 基于BMC的Web服务失配检测方法研究,TP311.52
  7. 基于SOA与工作流的OA系统的研究与实现,TP311.52
  8. 基于语义的Web服务发现研究,TP393.09
  9. 行政审批电子监察系统数据交换的设计与实现,TP311.52
  10. 嵌入式网络视频应用技术的研究与实现,TP368.1
  11. 一个试卷生成系统的设计与实现,TP311.52
  12. 公安信息系统中数据集成的,TP311.52
  13. 基于Web服务的Legacy System集成方法研究,TP393.09
  14. 基于Web服务的多平台实时票务系统的研究与实现,TP393.09
  15. 基于四方的安全电子商务支付协议研究,TP393.08
  16. 基于FPGA的SOPC视频复用器设计与实现,TN949.197
  17. 普适关爱系统的设计与实现,TN929.5
  18. 基于wifi的嵌入式视频监控系统设计,TP277
  19. 水土保持自动监测信息系统研究与实现,TP311.52
  20. 基于PLSA语义聚类的web服务发现方法,TP393.09
  21. 基于QoS感知的Web服务组合,TP393.09

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