随着Web服务技术的迅速发展,越来越多的Web服务运行在Internet上,这些单一的Web服务功能有限,不能满足用户的需求,但是这些单个、基本的Web服务,允许其他应用程序通过互联网连接及调用,组装成更复杂的应用以便用于表达业务流程。因此,如何确保组合起来的Web服务的正确性,成为Web服务研究领域中的热点。形式化方法在对基于消息通信和并发系统建模和分析方面已经成为非常重要的手段,其中模型检测作为一种自动验证技术被许多学者应用于Web服务组合的验证。　　 本文首先介绍了模型检测和时态逻辑的基本概念及业务流程执行语言(BPEL)和时间自动机的相关知识,并基于模型检测方法对Web服务组合验证开展研究,完成的主要工作如下：⑴在分析LSC的语法和基于路径的语义基础上,改进了LSC图到时态逻辑公式的转换方法,得到较短的时态逻辑公式,以便降低传统的模型检测对Web服务组合进行验证的复杂性。⑵提出了一种基于LSC的Web服务组合验证方法。该方法首先扩展了WS-BPEL的时间属性,并给出了BPEL描述的业务流程到时间自动机网络转化方法;其次,对LSC语法及语义进行时间属性方面的扩展,Web服务组合需要满足的场景用扩展后的LSC图来描述,并将LSC图转换为观察时间自动机;最后,通过将观察时间自动机与BPEL转化来的时间自动机网络同时嵌入到模型检测工具UPPAAL中,完成BPEL描述的业务流程是否满足LSC表示的性质的检测。⑶通过一个实例并使用UPPAAL工具对转换后的Web服务组合和场景性质进行验证。实例分析表明了本文给出的验证方法的有效性。