Service Oriented Architecture (SOA) is the most important and effective software paradigm to design Internet-based services. Using the SOA technology, value-added services can be easily deployed as a combination of existing Web services. In this context, WS-BPEL language has become the SOA industrial standard. To allow services to be composed, business relationships between providers and consumers have to be adequately managed. This implies that a formal definition of Quality of Service (QoS) is agreed and that effective tools for its measurement have to be developed. However, the design of QoS guaranteed composed Web services still requires several efforts due to the highly distributed nature of such software applications. This work aims at proposing a methodology to evaluate Web service performance at the earliest design phase. We present a novel technique to translate WS-BPEL processes into non-Markovian stochastic Petri nets with the final goal to evaluate parameters such as service time distribution and service reliability. The obtained model can be numerically solved through automatic tools, allowing to investigate the service behavior under different operating conditions and thus helping software engineers to develop QoS-guaranteed software solutions.