Behavior modeling and automated verification of Web services

Quan Z. Sheng*, Zakaria Maamar, Lina Yao, Claudia Szabo, Scott Bourne

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

23 Citations (Scopus)


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.

Original languageEnglish
Pages (from-to)416-433
Number of pages18
JournalInformation Sciences
Publication statusPublished - 10 Feb 2014
Externally publishedYes


  • Cloud computing
  • Conversation message
  • Service behavior
  • Symbolic model checking
  • Web service


Dive into the research topics of 'Behavior modeling and automated verification of Web services'. Together they form a unique fingerprint.

Cite this