To achieve a new web service functionality based on already existing web services, we need to describe a web service composition which consists of not only a set of interface collaborations among the web services but also a set of internal behaviors of the web services like a business process. But the description of a web service composition should be verified in terms of the correctness or time-related properties while representing internal and external behaviors which are written in xml-based standards, such as WSBPEL or WS-CDL. In this paper, a verification method is proposed which evaluates the choreography and the composition of the orchestrations for a web service composition. For that purpose, this paper provides a transformation method from orchestration descriptions and a choreography description to a set of formal state-based models. Moreover, we suggest analysis guidelines to evaluate the static and dynamic properties of the expecting web service composition through checking the simulation results.