On the one hand, Petri net models have a successful history in the modeling, simulation, and verification of workflows and business processes. On the other hand, BPEL is the de facto standard for describing and implementing Web service-based business processes. With abstract BPEL processes, BPEL can also be used as modeling language. However, being a complicated language with many syntactic constraints, abstract BPEL processes impede a straightforward modeling. In this paper, we introduce a fully-automatic translation of Petri net models into abstract BPEL processes which can be easily refined to executable BPEL processes. This approach combines strengths of Petri nets in modeling and verification with the ability to execute and port BPEL processes. Furthermore, it completes the Tools4BPEL framework to synthesize BPEL processes which are correct by design.