LTSA BPEL4WS plugin tutorial

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

Installing the application and plug-in

Download the latest version of the plug-in specified in the prerequisites above, then;

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 JDK 1.4 or higher installed, and that java is in your system path.

The LTSA-BPEL4WS Plug-in

On the main LTSA application window, there will be a tab labelled WS Compositions. If this does not appear, then there has been a problem loading the plug-in - try reinstalling using the previous procedure. Click on the image below to see the LTSA main application window.

From the LTSA main application window frame select the WS Compositions tab. The plug-in views will be displayed. Note that the pane is divided into several views. Left down and right down are the following panes:

Also note that there is a bar of buttons below the BPEL4WS Xml Text View and above the list views. This button bar provides shortcuts to various tasks described in the following topics.

Loading a BPEL4WS process file

To load a BPEL4WS process, click the Add button on the Composition List view. When you have selected a BPEL4WS XML file, each window pane (listed in the previous topic) will be updated. Notice how the BPEL4WS process is now represented as a XML DOM tree, a text file, and a series of actions. The WSDL for this BPEL is automatically loaded if named the same as the BPEL4WS file and is located in the same directory.

Editing the BPEL4WS process

To edit a BPEL4WS process, click the Edit button on the Composition List view. The BPEL4WS Xml Text View provides a simple text editor for changing the BPEL4WS Xml document. Note: as you change the BPEL4WS you may wish to periodically check that it is still valid XML and BPEL4WS. You can do so by clicking on the "Refresh Tree" and "Check" buttons at the bottom of this view.

Navigating the BPEL4WS process

Simple navigation can be performed on the BPEL4WS process by expanding the BPEL4WS Xml Tree View nodes. This can sometimes be easier than scrolling through the BPEL4WS XML Text View.

Checking the BPEL4WS process

Click on the "Check Source" button on the button bar below the BPEL4WS XML Text View. Results of checking will be displayed in the Progress/Warnings view.

Selecting an MSC specification (for design verification)

Click on the "SELECT SPEC FSP" button on the button bar below the BPEL4WS XML Text View. This will load the specification FSP file and update the Action List mapper to allow matching of actions in the BPEL4WS with that in the Specification. See the sample verification steps at the end of this tutorial for further process of mapping.

Generating the Finite State Process (FSP) for a composition

To generate an FSP representation of the BPEL4WS, click on the

button on the LTSA main application window toolbar. This will generate the FSP notation in the Edit pane. Further information about the generation of the FSP representation can be seen on the Output pane.

Sample Verification Steps of a BPEL4WS Process against an MSC Specification

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

This step requires the LTSAMSCPlugin for LTSA. Please refer to the MSC Editor tutorial for further details of download, installation and use of this editor.

Using the MSC Editor, create a hMSC with one bMSC (labelled for example as Echo). Create a new transition from init to the new bMSC (e.g. Echo).

Next, specify one scenario for the Echo bMSC. Create two instances, one named Caller and the other named Echoservice. Create two message links, one named receive.echo.message, from the Caller instance to the Echoservice instance. The other message link should be named reply.echo.message, from the Echoservice to the Caller instance.

Select the Edit pane in the LTSA main window and click on the Compile MSC button, which will generate the FSP representation of this MSC scenario. The FSP should then be saved (using File -> Save As) as echosample.lts.

Select the File -> Open menu item and select the echo.bpel from the samples directory. Alternatively the following XML represents this BPEL4WS and can copied directly into the BPEL4WS XML Text View pane of the BPEL4WS Editor.

</variables>

</partners>

</sequence>

</process>

Step 3. Select the Specification File and assign Mappings

Click the "SELECT SPEC FSP" button and select the echosample.lts file saved in step 1.

The Action List window will be updated, displaying this filename and updating the selectable map (relabel) names in the listbox. Select corresponding mappings for the following:

BPEL4WS Action	Specification Action
receive.caller.echoreceive	receive.echo.message
reply.caller.echoreply	reply.echo.message

This step is illustrated below.

Step 4. Generate the BPEL4WS FSP

This step compiles and creates the FSP represenation of the BPEL4WS and includes the specification FSP.

Click on the button on the LTSA main application window tool bar and the pane will change to the Edit pane listing the FSP representation.

Step 5. Perform a trace equivalence of the BPEL4WS and Specification

From the model combobox, select the CheckBPEL model. Then, from the Check menu select the Safety menu option.

The output will display any violations or dead-locks encountered in the trace equivalence.

Also, by selecting the BPEL model from the combobox, selecting Compile FSP button, and moving to the Draw pane, you can see a graphical representation of the BPEL process model. In our example it is simply two actions for receive and reply.

LTSA-BPEL4WS:

Tutorial 1

Model-based Verification of Web Service Compositions

Prerequisites