Behavior modeling and automated verification of Web services

Cloud computing has been rapidly adopted over the last few years. However, techniques on Web services, one of the most important enabling technologies for cloud computing, are still not mature yet. In this paper, we propose a novel approach that supports dependable development of Web services. Our approach includes a new Web service model that separates service behaviors into operational and control behaviors. The coordination of operational and control behaviors at runtime is facilitated by conversational messages. We also propose an automated service verification approach based on symbolic model checking. In particular, our approach extracts the checking properties, in the form of temporal logic formulas, from control behaviors, and automatically verifies the properties in operational behaviors using the NuSMV model checker. The approach presented in this paper has been implemented using a number of state-of-the-art technologies. We conducted a number of experiments to study the performance of our proposed approach in detecting design problems in services. The results show that our automated approach can successfully detect service design problems. Our system offers a set of tools assisting service developers in specifying, debugging, and monitoring service behaviors.