中文摘要：

形式化的分析有助于Web服务的合成．已有的合成分析方法，验证的重点是Web服务合成时形成的全局交互流程是否与预先定义的模型相匹配，忽略了合成时各个Web服务之间的行为是否相容．通过自动机对基于WSCI规范描述的web服务进行形式化描述．在此基础上，提出了一个Client／Server模型，定义了web服务合成的相容性概念，并提供相应的算法进行验证，保证了web服务合成的正确性．在相容性分析的基础上，考虑到web服务动态性的特点，定义了Web服务的替换性概念，并给出了保证替换服务正确性的定理．

英文摘要：

It is evidenced that formal analyses are helpful for Web services composition. Current analytical methods put the emphasis on checking whether the generated global interactive process during Web services composition is consistent with the predefined composite model, ignoring whether the respective behaviors of Web services are compatible. Through formalizing description of Web services based on WSCI by using automata, the Client/Server model is proposed built on the model of Web services, the concept of compatibility is defined, and the corresponding algorithm is developed, which can ensure the correctness of Web services composition. Also, because of dynamic features of Web services, the concept of substitutability is defined based on the concept of compatibility, and a theorem to ensure the correctness of substitute Web services is proposed.