Analysis of WS-BPEL Processes in PRISM

WS-BPEL has emerged as the de facto industry standard for composing Web services. With the wide attention for WS-BPEL, Quality of Service (QoS) for it has become a key differentiator to judge the services with same functionalities. One main challenge currently is how to analyze the QoS of WS-BPEL services at the early design phase. This work aims at proposing a methodology for model-based analysis of WS-BPEL processes, with a focus on the assessment of non-functional quality attributes. Particularly, we define a small language BPELR to model the core features of WS-BPEL language, and annotate message receiving and service invoking activities with message-arrive rate and service-execute rate separately. Then a set of rules are proposed for translating BPELR into the input language of the probabilistic model checker PRISM, which can be used to stochastically analyze WS-BPEL processes. Finally, we show our approach by a purchase order business process example.