Probabilistic Timed Model Checking for Atomic Web Service

As Web services are becoming more and more complex, there is an increasing concern about how to guarantee the correctness and safety of Web services composition. This has driven many researchers to study the performance analysis of dynamic atomic service selection, as well as functional verifications. In this paper, we focus on not only modeling the behaviors of atomic service, but also verifying the properties in a quantitative way. First, we apply probabilistic timed model checking to model and verify the behaviors of atomic service by extending interface automata, and propose a technique to formally estimate software performance which exhibits stochastic behaviors with time constrains. Second, the probabilistic timed computation tree logic (PTCTL) formulae are used to express the reliability properties. Third, a failure may occur stochastically when an invocation is triggered through interface operation. We present an internal interaction model, based on which we can dynamically pick out a highest reliable execution sequence for Web services composition. Finally, a case study is demonstrated and experimental results are discussed. In conclusion, our approach provides with an underlying guideline for Web services composition.