An approach for modeling Web service composition by Petri nets which is based on OWL-S is proposed. By this approach, first, control flow of the composite web service is modeled based on top-down method. Then data flow model is constructed with Petri nets according to data flow specification. After that, by using a bottom-up approach, synchronous composition, the data flow net of the composite service is combined with the control flow net to obtain an integrated service net. So, the details can be introduced in an incremental way. Moreover, based on modeling approach, the boundedness and liveness properties of Petri net models are analyzed for guaranteeing the correctness of the composite Web service. Analysis and verification technique is based on the properties preservation criteria such that complexity is alleviated. Finally, an application of the proposed approach is presented for modeling a case study: BuyOnline Web service.