The case study is a very simple but sufficient to show how BASIS works. This ATM service is modified from the original version (see full ATM service) in order to be supported by most of the BPEL engines. The target service code of this case study can be downloaded here, which is also available in the download page.

The ATM service animates one possible implementation of the Automation Teller Machine that people can use to deposit and withdraw money. Customers of the service send connect requests with an identification string. After receiving the reply from the ATM, the customer can logon to the ATM, and then choose to withdraw or deposit some money. After receiving the reply of the operation, the customer logoff from the ATM and finally disconnect the connection.

In the following, there the activity diagram of the behavior of the ATM service. To the right of it, is the constructed BPN model (Petri-net based model for BPEL services).

The user behavior requirement of the ATM service is the withdrawal scenario depicted in the following figure, which is a Rational Rose UML Sequence Diagram. The Sequence Diagram represents the withdrawal behavior: after the client logon to the service, some money is successfully withdrawn from the ATM, and then the client logoff from the service and disconnects the connection. In the Sequence Diagram, “_this:_Process” stands the service itself while other communication partners are represented by the form partnerLink: partnerLinkType as in the BPEL definition. In this case, the client is the “atmFrontEnd: atmFrontEndPLT”.

The target service (including BPEL and associated WSDLs and XML Schema), user scenario requirement (UML Sequence Diagram) are provided as input to the BASIS v0.1.0. It will first generate the BPEL-Petri-nets model (BPN model for short) as shown in the above, then perform the behavior analysis on BPN model against user scenario. The behavior analysis result of the ATM service and withdrawal scenario is a set of paths Δ(N, D), where N is the ATM BPN model and D is the withdraw scenario.

There is only one path in Δ(N, D) = {ρ0}, where the segment of the path in bold are the exact image segment:

ρ0  =   μ0: { p0 } –τ0: {t0}→ μ1: { p1 } –τ1: {t1}→ μ2: { p2 } –τ2: {t2}→ μ3: { p3 } –τ3: {t7}→ μ4: { p8 } –τ4: {t8}→ μ5: { p5 } –τ5: {t5}→ μ6: { p6 } –τ6: {t6}→ μ7: { p7 }

The behavior constraint automaton X(N, D) is as the following figure:

The manipulator services are then constructed. Sample input to the BASIS v0.1.0 tool is given in the picture in intruduction page, where the first three inputs are the file locations, and the manipulation choice is made on Behavior extraction. The constructed manipulator services of this case study can be downloaded from: ATM-Withdrawal manipulator sample*. The structure of generated manipulator services and files is: