Model Checking Behavioral Specification of BPEL Web Services
Rongsheng Dong, Wei Min Zhao, Xiangyu Luo · 2008
Abstract—BPEL is a business flow language which describes the composition of web services. Since business flow may be very complex, the method of formalized analysis can help ensure the accuracy of work flow. For web services described by BPEL, in this paper we establish a formalized analysis model, provide specifications and semantics of business flow, and finally translate it into the asynchronous communication model of the model checker SPIN. Based on the formalized analysis model proposed in this paper, we analyze and verify the SAS [1], Loan and Auction protocols [2], and detect a flaw in the data flow of SAS protocol.