本文的研究工作包含两个部分:第一,对Web服务组合的正确性进行了验证,提出了基于BPEL的Web服务组合形式化分析模型和自动测试框架;第二,对Web服务的安全性进行了形式化分析,建立了基于SOAP的安全协议的形式化分析模型,验证了WS-Secure Conversation协议的安全属性。主要研究成果如下:　　(1)基于有限状态自动机理论,提出了BPEL的Web服务组合的形式化分析模型,定义了BPEL业务流的规格和语义,给出了分析模型转化为Promela代码的方法。使用该模型分析了SAS协议,用模型检验工具SPIN验证了协议的无死锁、可达性和活性,发现了该协议存在的一个功能缺陷;采用该模型分析了BPEL2.0中的Loan、Auction协议,验证了协议的活性。　　(2)根据模型检验自动生成反例的特性,在本文提出的Web服务组合的形式化分析模型的基础上,建立了BPEL的Web服务组合自动化测试框架。该框架根据用例的输入、输出与需求属性对BPEL业务流的一致性进行测试,并以机票预定系统为例,测试了该系统的一致性。　　(3)使用模型检验技术,建立了基于SOAP的安全协议的形式化分析模型,给出了此类协议的抽取方法,对能操纵SOAP消息中的XML元素的攻击者进行了描述。以WS-Secure Conversation协议为例,使用该模型验证了协议的认证性和秘密性,发现该协议存在认证性的缺陷。针对该缺陷,对协议的消息结构进行了修改,并对用户口令进行了数字签名,避免了原协议的缺陷。