Go to directory wsatDemo-1.0/Samples/BPEL_Examples/loan_approval_process.
type the following command, the Promela translation will be generated for the composition of four BPEL web services: a loan approval process, a risk assessor, a back-end approver, and a customer. Note that the loanapproval.bpel is the loan approval process given in the BPEL4WS standard, and we supplied the "dummy" BPEL services for the other three peers.
The shell script actually contains the following command:
java wsat -BPEL loanapproval loanapproval.wsdl
loanapproval.bpel assessor loanassessor.wsdl loanassessor.bpel approver
loanapprover.wsdl loanapprover.bpel customer loanassessor.wsdl customer.bpel
-MAPENTRY approver customer loanapproval approver loanapproval -MAPENTRY
customer approver loanapproval -MAPENTRY assessor customer loanapproval
Note that after "-BPEL", we specified four interacting BPEL peers, each peer consists of three parts: its name, its WSDL declaration, and its BPEL specification. For example, peer "loanapproval" has the "loanapproval.wsdl" and "loanapproval.bpel" specifications. The -MAPENTRY establishes the communication channels between peers. For example "-MAPENTRY customer approver loanapproval" means that for the peer "customer", the role "approver" in its BPEL specification should corresponds to peer "loanapproval".
1. LTL model checking
After running exec.sh, output.pml contains the Promela translation of the BPEL web service composition. You can use "spin -t" to generate any desired LTL properties, and verify them following the steps given in the instructions for the SAS example.
2. Synchronizability Analysis
Decision procedure for the relaxed autonomous condition [WWW'04] will be ready soon. We will give a detailed explanation of the synchronizability analysis HERE.
(last updated: July 9, 2004)