Process of service composition is complex and error-prone, which makes a formal modeling and analysis method highly desirable. This paper presents a Petri net-based approach to analyzing the soundness and compositionality of services in BPEL. A set of translation rules is proposed to transform BPEL processes into Petri nets, by which behaviors of the BPEL processes are articulated.??The instantiation net of target services are used to capture all of the possible implementation flows of composition processes. Based on theories of Petri nets, the principles for analyzing soundness and compositionality of Web services are provided. A detailed example is given to demonstrate the applicability of our method.