The bpel4ws plugin is an extension to LTSA (and LTSA-MSC) that allows the creation of models of BPEL4WS processes, driven by a formal behaviour model.
This tutorial contains:
The following are required to complete this tutorial:
Download the latest version of the software specified in the prerequisites above, then;
%JAVA_HOME%\bin\java -cp .;lib\jdom.jar;lib\ltsa.jar;lib\custom.jar;lib\scenebeans.jar;lib\jel.jar;lib\xml.jar;lib\LTL2Buchi.jar;lib\bpws4j.jar;lib\xml-apis.jar;lib\log4j-1.2.4.jar;lib\xercesImpl.jar;lib\wsdl4j.jar;lib\jaxrpc.jar ic.doc.ltsa.HPWindow
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.
On the main LTSA application window, there will be tab labelled BPEL Editor. If this does not appear, then there has been a problem loading the plugin - 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 BPELEditor tab. The BPEL4WS Editor pane will be displayed. Note that the pane is divided into 4 sub-panes. From left to right clockwise are the following panes:
BPEL4WS XML Tree View
BPEL4WS XML Text View
Editor Status Window
Action List Window and Mapper
Also note that there is a bar of buttons below the BPEL4WS Xml Text View. This button bar provides shortcuts to various tasks described in the following topics.
To load a BPEL4WS process, select File -> Open from the menu bar. 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 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.
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.
Click on the "Check" button on the button bar below the BPEL4WS XML Text View.
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.
To generate an FSP representation of the BPEL4WS, click on the
button on the LTSA main
application window. 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.
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.
Step 1. Create the Specification and behaviour model using MSCPlugin
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.
These steps are illustrated in the figures below.
 |
|
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.
Step 2. Load / Create the BPEL4WS Process
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.
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.
