Web service is an emerging paradigm for distributed computing. First, in order to verify web services rigorously, it is important to provide a formal semantics for the flowbased web service language (WS). A suitable formal model should cover most features of the WS. The existing formal models either abstract from data, cover a simple subset of WS, or omit the interactions between certain components. This paper presents a web service automaton, an extension of Mealy machine, to fulfill the formal model requirements of the web service domain. Second, semantic compatibility checking between web services is another important issue. The existing checking approaches are post-checking, where the compatibility is checked after composition. As a complement to post-checking, we proposes anti-patterns for web service interactions as a pre-checking, so that certain incompatible web services can be modified or re-selected in the earliest stages.