Service composition, which provides a more effective way to combine several single services into a composite service, is a kind of software reuse techniques. However, one of the most important problems is how to perform service composition correctly and effectively so as to produce high-quality source codes for describing the resulted composite service. In this paper, we propose a model-driven method to solve this problem, where UML 2.0 sequence diagrams are extended to model the composition of web services, extended statecharts are synthesized from sequence diagrams, then the statecharts are further transferred to the input language of a model checker for behavior consistency checking, and finally verified BPEL codes can be generated from improved sequence diagrams. Case studies have been performed to demonstrate the whole process and illustrate the significance of our approach.