由于应用的复杂性，在很多情况下单个Web服务难以满足实际需求，对于复杂业务过程的处理需要采用服务组合的方法即由各个小粒度的Web服务相互之间通信和协作来实现大粒度的服务功能。Web服务组合常用于描述跨组织的业务流程等高层业务逻辑，这意味着系统的任何错误都可能导致严重的损失。保证服务组合的正确性，确认服务组合的有效性是Web服务组合系统成功的关键。 本文将基于自动机的模型检查技术应用到Web服务组合中。首先从语义角度研究了PROMELA语义引擎问题。PROMELA语言是模型检查工具SPIN的核心，对PROMELA语言执行方式的理解决定所描述系统模型的行为方式。论文给出PROMELA语法的抽象对象模型的形式化定义和一个算法来实现PROMELA语法到抽象对象模型的映射，描述了PROMELA指称语义。针对SPIN中原子序列和同步通信等复杂问题给出了解决方法。 然后提出了对基于WS—CDL的Web服务组合的PROMELA建模与验证。WS—CDL支持的控制流机制包括：顺序、并发、同步、条件、非确定性选择等。论文提出了一种Web服务数据流和控制流的模型，可以在数据流和控制流之间验证不利的交互。WS—CDL进程模型的PROMELA映射关键在于WS—CDL进程模型验证相关方面的确定以及如何执行这种映射。 最后利用模型检验工具SPIN对有第三方支付平台参与的网上交易进行形式化分析。实验证明此方案能够对基于WS—CDL的Web服务组合进行行之有效的验证。