The case study code is taken from the ActiveBPEL Engine examples and which is taken from the Example section of WS-BPEL specification.
This example consists of a simple loan approval service. Customers of the service send loan requests, including personal information and amount being requested. Using this information, the loan service executes a simple process resulting in either a "loan approved" message or a "loan rejected" message. The decision is based on the amount requested and the risk associated with the customer. For low amounts of less than $10,000 a streamlined process is used. In the streamlined process low-risk customers are approved automatically. For higher amounts, or medium and high-risk customers, the credit request requires further processing. For each request, the loan service uses the functionality provided by two other services. In the streamlined process, used for low amount loans, a risk assessment service is used to obtain a quick evaluation of the risk associated with the customer. A full loan approval service (possibly requiring direct involvement of a loan expert) is used to obtain assessments when the streamlined approval process is not applicable.
The verification process is illustrated in the following figure. Firstly, we take theWS-BPEL files of Web Services as input. Then we simplify theWS-BPEL code and transform the WS-BPEL process to the Petri net models. After that we get the simplified Petri net models by doing the simplification for the Petri net models in last step. The simplified Petri net models are used for the consistency verification against the input scenario specification expressed by the UML Sequence Diagrams. Finally the verification result is given.
The WS-BPEL file is firstly simplified. The aim of simplification is to remove all fault, compensation and termination handlings (FCT-handling), empty activities and merge immediately assignments. The original WS-BPEL code and simplified WS-BPEL code is listed as follows.
| The original WS-BPEL code | The simplified WS-BPEL code |
|
|
|
The simplified WS-BPEL file is then transformed into Petri net model and the Petri net is also simplified to remove redundant places and transitions. In the following figure, the Petri net is presented. And you can download the generated PNML file here.
Three Rational Rose UML Sequence Diagrams are provided as scenario-based specifications for verification. The files are assessorUSD.mdl, approvalUSD.mdl and replyUSD.mdl in the archive file of the case study (can be downloaded in the download page). These three sequence diagrams can either be used for existential consistency checking or mandatory consistency checking. Here we give results of two examples. Scenario 1 is to check the existence of invoking the loan approver service and receiving reply from it, i.e. to perform existential consistency checking of approvalUSD.mdl. Scenario 2 is to check wheter replying the customer immediately follows the invocation of assesment service (and receiving reply from it), i.e. to perform forward mandatory consistency checking of assessorUSD.mdl (as SD1) and replyUSD.mdl (as SD2).
The checking result of Scenario 1:
Three paths are presented here, note that only the id of transitions are shown:
E.g. 1: (φ0)t0 ^ (φ1)t1 ^ (φ2)t3 ^ (φ3)t4 ^ (φ4)t5 ^ (φ5)t12 ^ (φ6)t13 ^ (φ7)t14
E.g. 2: (φ0)t0 ^ (φ1)t1 ^ (φ2)t3 ^ (φ3)t16 ^ (φ4)t17 ^ (φ5)t12 ^ (φ6)t13 ^ (φ7)t14
E.g. 3: (φ0)t0 ^ (φ1)t1 ^ (φ2)t3 ^ (φ3)t4 ^ (φ4)t5 ^ (φ5)t6 ^ (φ6)t7 ^ (φ7)t12 ^ (φ8)t13 ^ (φ9)t14
And if the scenario is satisfied, transitions t0, t1, t3, t12, t13, t14 must be fired, while transitions t0, t1, t3, t4, t5, t6, t12, t7, t13, t14, t11, t16, t17 can possibly be fired in some order.
The checking result of Scenario 2:
Three paths are presented here, note that only the id of transitions are shown:
E.g. 1: (φ0)t0 ^ (φ1)t1 ^ (φ2)t3 ^ (φ3)t4 ^ (φ4)t5 ^ (φ5)t6 ^ (φ6)t7 ^ (φ7)t12 ^ (φ8)t15 ^ (φ9)t8 ^ (φ10)t9
E.g. 2: (φ0)t0 ^ (φ1)t1 ^ (φ2)t3 ^ (φ3)t4 ^ (φ4)t5 ^ (φ5)t6 ^ (φ6)t11 ^ (φ7)t12 ^ (φ8)t15 ^ (φ9)t8 ^ (φ10)t9
E.g. 3: (φ0)t0 ^ (φ1)t1 ^ (φ2)t3 ^ (φ3)t4 ^ (φ4)t5 ^ (φ5)t12 ^ (φ6)t15 ^ (φ7)t6 ^ (φ8)t7 ^ (φ9)t8 ^ (φ10)t9
And if the scenario is satisfied, transitions t0, t1, t3, t4, t5, t12, t6, t15, t8, t9 must be fired, while transitions t0, t1, t3, t4, t5, t12, t6, t15, t11, t8, t9, t7 can possibly be fired in some order.