Web服务可视为具有并发性的分布式软件系统,可通过相关标准实现不同应用程序间的互操作。然而,并发系统往往存在非确定性进程调用,程序员在编写代码时很难考虑到大量并发进程中所有可能的交互,致使写出的程序的正确性和可靠性难以得到保证。因此Web服务的形式化分析和验证就显得尤为重要了。　　考虑到Web服务具有软件的特性,本文应用软件模型检测技术对其进行形式建模和验证。为了提高Web服务流程建模的自动化程度,本文提出将描述Web服务组合的流程语言BPEL4WS转化到软件模型检测工具ZING的输入语言的一系列转换算法,最后在ZING环境下对虚拟旅行系统和贷款服务协议进行形式化建模和验证,从而论证本文所提出方法的正确性及有效性。本文的工作主要体现在以下几个方面:　　(1)本文分析了BPEL的相关属性和活动特征,同时考虑软件模型检测工具ZING的输入语言特点,提出了便于将BPEL语言转化到ZING输入语言的形式化模型—输入输出标号迁移系统I/OLTS,为实现形式建模的自动化打下基础。　　(2)建立BPEL活动和I/OLTS间的一一对应关系和转化规则,从而实现BPEL向形式模型的自动转化。　　(3)提出了从中间形式模型I/OLTS自动生成ZING输入语言的转化算法。该算法根据I/OLTS本身特性和ZING输入语言的特性,将I/OLTS中包含的各个元素逐一的转化为ZING的输入语言,实现了I/OLTS到ZING输入语言的自动转化。　　(4)应用所提出的方法对虚拟旅行系统和贷款服务协议的安全性和死锁问题进行验证,找出其中存在的错误或漏洞。