Web services have become the technology of choice for service-oriented computing implementation, where Web services can be composed in response to some users' needs. It is critical to verify the compatibility of component Web services to ensure the correctness of the whole composition in which these components participate. Traditionally, two conditions need to be satisfied during the verification of compatibility: reachable termination and proper termination. Unfortunately, it is complex and time consuming to verify those two conditions. To reduce the complexity of this verification, we model Web services using colored Petri nets (PNs) so that a specific property of their structures is looked into, namely, well structuredness. We prove that only reachable termination needs to be satisfied when verifying behavioral compatibility among well-structured Web services. When a composition is declared as valid and in the case where one of its component Web services fails at run time, an alternative one with similar behavior needs to come into play as a substitute. Thus, it is important to develop effective approaches that permit one to analyze the similarity of Web services. Although many existing approaches utilize PNs to analyze behavioral compatibility, few of them explore further appropriate definitions of behavioral similarity and provide a user-friendly tool with automatic verification. In this paper, we introduce a formal definition of context-independent similarity and show that a Web service can be substituted by an alternative peer of similar behavior without intervening other Web services in the composition. Therefore, the cost of verifying service substitutability is largely reduced. We also provide an algorithm for the verification and implement it in a tool. Using the tool, the verification of behavioral similarity of Web services can be performed in an automatic way. © 2006 IEEE.