【摘 要】
：
Web服务作为一种新的计算模型正受到越来越多的关注,保证Web服务组合执行结果的一致性和可靠性是Web服务面临的重要挑战之一。将事务机制应用到Web服务领域是寻求解决Web服务
论文部分内容阅读
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生成的反例。
其他文献
随着通信技术近些年的迅猛发展,层出不穷的无线通信系统为用户提供了异构的网络环境。然而不同的接入技术在带宽、传输时延、覆盖范围以及移动性支持等方面存在差异,没有一种
图像分割是计算机视觉领域中一个重要的研究方向，是进行图像分析和图像识别的前提。主动轮廓模型改变了传统图像分割的思想，它在进行图像分割的过程中结合了先验知识，吸引了大量
移动计算系统的移动性、灵活性、自治性等特点使其具有了更加广阔的应用前景,但是由于移动设备的不可靠性和无线链路连接的脆弱性,降低了移动计算系统的可靠性。检查点卷回恢
近年来,分组交换网络技术和语音通信技术都取得了长足的发展,先进的语音通信技术不断被提出和改进,分组交换网络的规模和传输速度不断提升,同时这两者也在不断交叉渗透,相互
电力产业在国民工业系统中具有支柱作用,电力的平稳运行关乎国民经济的命脉。在电力系统管理中,电力负荷预测至关重要。准确的电力负荷预测能够为电力系统的平稳运行、制定合理电价、电力实时调度提供重要依据。特别是在经济领域,电力负荷预测能够对合理调配资源,优化发电计划,取得最优的社会效益和经济效益起到巨大作用。然而随着我国经济的快速发展,对电力的需求日益增长,电力负荷本身也受日期、天气、气候、市场以及政策影
随着科技的迅猛发展,人类已逐渐步入一个全新的数字化时代,虚拟现实技术给人们带来了一种全新的沉浸式的体验。为了让用户能获得更好的虚拟现实体验,虚拟出来的画面一定要有
随着信息技术的发展,特别是Web技术的发展,对网络上的服务器提出了越来越高的要求,越来越多的瓶颈会出现在服务器端。集群技术是实现高性能服务的一种有效途径。服务器集群负
软件水印是一种新型的软件版权保护方式,与仅仅依赖于加密技术的传统的软件版权保护方法不同,它是通过在软件代码中嵌入某些特定的秘密信息,在必要的时候,可以从软件中提取出
视频目标跟踪作为计算机视觉领域的基础问题,一直以来都是学者们的研究热点。其中视频中目标的观测模型又是视频目标跟踪问题的一个重要组成部分,已经有大量关于目标观测模型
发布/订阅(Publish/Subscribe,P/S)通信范型具有异步、多点通信等优点,一直受到学术界和工业界的普遍关注。传统有线网络中的发布/订阅系统的研究相对比较成熟,在金融、物流