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.　©　2011　IEEE.