To address state space explosion and the inability to automatically generate the BPEL (business process execution language) codes of the existing methods of composing services based on mediators, this paper presents an approach to verify the Petri net models of service composition by modular reachability graphs. In this approach, the Petri net models of service composition are divided into sub-models in a modular way, and verify the feasibility of composition by analyzing the state spaces of individual sub-models, without unfolding to the ordinary state space. Using this modular technique can avoid the state space explosion. After verification of the feasibility, the paper proposes a method of automatically generating the BPEL codes of the whole composite service from the Petri net models of composition. The main idea is to generate the BEPL codes from the fused transitions between the sub-models based on ECA rules. Finally, an application of the methods is illustrated though a case study in an e-business enterprise.