Abstract: The existing works can not verify whether the composed service's function, response time and cost satisfy requester's requirement simultaneously,and treat it separately. We extended basic workflow patterns in order to depict probabilistic choice, stochastic time and nondeterministic choice of composed cloud services. An approach to mapping the extended patterns to continuous time Markov reward process was proposed. The existing temporal logic CSRI. was extended for specifying the specifications which can depict function,response time and cost constraints,and the stochastic model checking approach was proposed. This paper shows that we can depict cloud service's runtime dynamic behaviors effectively and verify their correctness and availability.

Key words: Cloud service, Workflow, Markov processes, Stochastic model checking