web服务线性态逻辑模型检查研究.pdf

摘 要 由于应用的复杂性，在很多情况下单个Web服务难以满足实际需求，对于复 杂业务过程的处理需要采用服务组合的方法即由各个小粒度的Web服务相互之 间通信和协作来实现大粒度的服务功能。Web服务组合常用于描述跨组织的业务 流程等高层业务逻辑，这意味着系统的任何错误都可能导致严重的损失。保证服 务组合的正确性，确认服务组合的有效性是Web服务组合系统成功的关键。 本文将基于自动机的模型检查技术应用到Web服务组合中。首先从语义角度 PROMELA语言执行方式的理解决定所描述系统模型的行为方式。论文给出 PROMELA语法的抽象对象模型的形式化定义和一个算法来实现PROMELA语法到抽 象对象模型的映射，描述了PROMELA指称语义。针对SPIN中原子序列和同步通 信等复杂问题给出了解决方法。 支持的控制流机制包括：顺序、并发、同步、条件、非确定性选择等。论文提出 了一种Web服务数据流和控制流的模型，可以在数据流和控制流之间验证不利的 的确定以及如何执行这种映射。 最后利用模型检验工具SPIN对有第三方支付平台参与的网上交易进行形式 化分析。实验证明此方案能够对基于WS-CDL的Web服务组合进行行之有效的验 证。 关键词：Web服务；线性时态逻辑：形式化方法；模型检查 Abstract A and web difficulttomeettheactualdemandin singlesimpleservice(WS)is casesduetothe deal谢tllthe business many complexi够ofapplications．To complex itneedsto anumberofWSs．A processes compose numberofWSsofsmall granularity communicateand collaboratewitlleachothertoachieve servicefunction．The complex ofWSsiSusedtodescribethecombinationof composition cross．organizational business as that business means processes，suchhigh-level logic，which system any errorscail to leadseverelossesandfaults．ThetoSuccessis ensureandconfirm key to the ofwebservices validity composition． Inthis model basedonautomatais to paper checkingtechnology applied of semanticofPROMELAis compositionWSs．First，the studied．PROMELA