This paper proposes a new verification method for individual web service specified using OWL-S, the Ontology Web Language for semantic web Services, where probabilities are introduced to model uncertain choices. The approach makes use of a probabilistic model checker named PRISM. The web service description is received as an input in form of OWL-S, which is analyzed and automatically transformed into a Discrete Time Markov Chain (DTMC) or a Markov Decision Process (MDP). The obtained DTMC/MDP is then processed and coded into the PRISM language. This code is parsed and verified by the PRISM model checker to determine which required properties are satisfied by the web service. In addition to the atomic processes, different composite processes are considered including sequence, choice, if-then-else, repeat-while, repeat-until, split, and split join. We also prove that the transformation algorithm is sound and complete and introduce a software tool implementing the approach.