随着以Web服务为基础的面向服务的体系结构的发展，如何有效组合自治的、分布的、不同功能的Web服务以构建新的企业业务应用逐渐成为热点。但是，Web服务组合技术的研究刚刚起步，还面临很多问题，比如Web服务如何组合，能否自动组合，组合的正确性验证，以及如何利用模型检测技术来解决诸如服务组合状态的终止性和可达性等问题。针对这些不足，本文将时序逻辑TLA(Temporal Logic ofActions)引入到Web服务组合验证的课题中，结合BPEL4WS(Business Process Execution Language for Web Services)描述语言，着重研究和讨论了如何将组合服务的BPEL描述文档转化为TIA表达式的问题，并在理论研究的基础上开发了一个转换工具以实现两者的自动转换。主要工作包括： 1) 将组合服务的BPEL流程转化为TIA表达式这是论文的研究重点。文中简单介绍了Conversation模型的概念，利用该模型作为中介，首先将组合服务的BPEL描述转化为Conversation模型，再将Conversation模型转换为TLA表达式，并给出了具体的算法。 2)转换工具的实现本文在理论研究的基础上开发了一个将BPEL转化为TLA的工具。该工具读入组合服务的BPEL文档，生成Conversation模型，再将其转化为TLA表达式并生成TLA文档。具体实现是在开源的Web服务验证工具WSAT的基础上进行的，沿用了WSAT的一些数据结构以及类的设计，修改了相关的代码以满足Conversation模型，添加了将状态自动机转化为TLA的程序模块。 3)实验和验证使用上述转换工具对特定的案例(雇员出差安排的BPEL流程)进行实验，将其转化为TLA表达式，再使用TLC(TLA中已有的验证工具)对系统进行“系统死锁”的验证。