Modeling and verification of Web services composition based on model transformation. (16th August 2016)

• Record Type: Journal Article
• Authors: Zhu, Yi; Huang, Zhiqiu; Zhou, Hang
• Is Part Of: Software, practice & experience. Volume 47:Number 5(2017)
• Page Start: 709
• Page End: 730
• Publication Date: 2016-08-16
• Subjects: formal verification -- model transformation -- Web services composition -- BPEL -- CSP; Computer software -- Periodicals; Computer programming -- Periodicals; Computer programs -- Periodicals; 005.3
• DOI: 10.1002/spe.2434
• Languages: English
• ISSNs: 0038-0644

Abstract

Summary: With the rapid development of Cloud computing, social computing, and Web of Things, an increasing number of requirements of complexity and reliability for modeling Web services composition have emerged too. As more reliable methods are needed to model and verify current complex Web services composition, this paper proposes a method to model and verify Web services composition based on model transformation. First, a modeling and verifying framework based on model transformation is established. Then, Communicating Sequential Process (CSP) is defined according to the features of Web services composition and the corresponding model checking tool Failure Divergence Refinement (FDR) is introduced. The transformation approaches between Business Process Execution Language (BPEL) and CSP are later defined in detail. Lastly, the effect of this method is evaluated by modeling and verifying the Web services composition of a Online Shopping System. The results of the experiments show that this method can greatly increase the reliability of Web services composition. Copyright © 2016 John Wiley & Sons, Ltd.