Abstract: 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.