LTSA-BPEL4WS:

Tutorial 2

Modelling Interacting Web Service Compositions

The bpel4ws plug-in is an extension to LTSA that allows the creation of models of BPEL4WS processes, driven by a formal behaviour model.

The home of the BPEL4WS plug-in is here.

This tutorial contains:

Overview of the features of the plug-in.
A step-by-step verification example of interacting BPEL4WS processes (with respect to their labelled transition system models).
Illustrated implementation of the work described in Compatibility Verification for Web Service Choreography (presented at the 2nd International Conference on Web Services, San Diego, July 2004).

Prerequisites

The following are required to complete this tutorial:

An installation of the LTSA tool (see here for required software components)
Walked through the setup and basic principles of using LTSA-BPEL4WS in TUTORIAL 1.
Tutorial 2 source files are located here for download and use in this tutorial.

Starting the application

In the root directory of the installation is a file called run.bat. Run this to start the application. If any exceptions are reported, check that you have correct Java Runtime or Development Kit installed (JRE/JDK 1.4 or higher), and that java is in your system path (also check JAVA_HOME variable points to the java installation directory).

Sample Modelling Steps of Interacting BPEL4WS Processes

This example provides a simple step-by-step process from creating/loading partnered BPEL4WS processes, mapping the two processes together and then generating verification traces by using the trace features of the LTSA tool.

Important Note: Please download the tutorial source files (described in the prerequisites section of this tutorial).

Step 1. Load the ECHOSTRING1 BPEL4WS process and WSDL service description

Switch to the WS Compositions tab (as illustrated in figure 1).
Locate the Composition List view and click the Add button.
Select the file \tutorial2\echobpel1.bpel (This should load both the BPEL4WS and the WSDL for the ECHOSTRING1 process). Verify that the process has loaded by viewing the process in the BPEL4WS XML Editor and WSDL Editor views.
Goto Step 2.

Figure 1. Loading BPEL4WS processes and WSDL service descriptions in LTSA-BPEL4WS.

Step 2. Translate and view process Labelled Transition System model

Locate the tab toolbar (directly below the main menu of the LTSA tool window).
Click the "BPEL4WS to FSP" button. Note that the translation will switch to the Edit tab and display the corresponding Finite State Process (FSP) notation for the ECHOSTRING1 process.
Select Build->Compose from the main LTSA menu options. Note that the compose option will switch to the Output tab for compilation results.
Switch to the Draw tab.
Select the ||ECHOSTRING1_BPELArchitectureModel from the list of processes in the left pane. The process illustrated in figure 2 should be shown.

Figure 2. Labelled Transition System model of the ECHOSTRING1 process.

Step 3. Load the ECHOSTRING2 BPEL4WS process and WSDL service description

Switch to the WS Compositions tab.
Locate the Composition List view and click the Add button.
Select the file \tutorial2\echobpel2.bpel (This should load both the BPEL4WS and the WSDL for the ECHOSTRING2 process). Verify that the process has loaded by viewing the process in the BPEL4WS XML Editor and WSDL Editor views.
Note that the Composition List view should now include both ECHOSTRING1 and ECHOSTRING2 processes.
Repeat Step 2 but selecting ||ECHOSTRING2_BPELArchitectureModel when viewing the model within the Draw tab pane, as illustrated in Figure 2.

Figure 2. Labelled Transition System model of the ECHOSTRING2 process.

Step 4. Manually verify that partner operations are related

Select the ECHOSTRING1 process in the Composition List view and click on the Edit button.
Scroll through the process and locate the construct: <invoke partner="echoprovider" portType="echoPT" operation="echo"....
Scroll through the process and locate the <partner> section - this should contain the partner entry for the "echoprovider" partner specified in the invoke operation. This partner specifies the use of the serviceLinkType "echoSLT" in the serviceLinkType declaration. This is defined in the WSDL interface for the partner process.
Scroll through the WSDL Editor view and locate the <slt:serviceLinkType> section.
Note that the portType for this serviceLinkType is "tns:echoPT". This is the link between local and partner process for this operation.
Select the ECHOSTRING2 process in the Composition List view and click on the Edit button.
Scroll through the WSDL Editor view and locate the <portType name="echoPT"> section. This is the related partner link to a remote operation.
Note that the portType section has a single operation entry for operation "echo". The operation specifies both input and output messages.

Step 5. Compose "unsynchronised" model of Process Architecture

Switch to the WS Compositions tab (if not already in view).
Click the "Compose All BPEL4WS" button . Note that the translation will switch to the Edit tab and display the corresponding Finite State Process (FSP) notation for the combined processes.
Select the Build->Compile from the main LTSA menu options - this action refreshes the list of processes in the listbox located on the toolbar.
Click the expand listbox button (to the right of the listbox) and select the "CompositionArchitecture" process.
Select Build->Compose from the main LTSA menu options. Note that the compose option will switch to the Output tab for compilation results.
Switch to the Draw tab.
Select the ||CompositionArchitecture from the list of processes in the left pane. The composition architecture model view is illustrated in figure 3.

Figure 3. Labelled Transition System model of an unlinked port (CompositionArchitecture) model process.

The model produced is an unlinked model of the combined processes.
Now we need a combined messaging model.

Step 6. Compose "synchronised" Model of Interacting Processes

Click the expand listbox button (to the right of the listbox) and select the "PortArchitecture_echostring1_echoslt_echo" process. This is the process of the port connector for the ECHOSTRING1 and ECHOSTRING2 "echo" operation.
Select Build->Compose from the main LTSA menu options. Note that the compose option will switch to the Output tab for compilation results.
Switch to the Draw tab.
Select the ||PortArchitecture_echostring1_echoslt_echo from the list of processes in the left pane.

Figure 4. Labelled Transition System model of a linked messaging port for the "echo" operation.

Switch to the Edit tab.
Repeat Step 6 but selecting ||PortArchitecture_echostring2_auditslt_echo in the process listbox.

Step 7. Now try modelling your own process interactions!.... and have fun!