In this tutorial the user will be able to analyse a WS-BPEL process for fulfillment of a Design Specification.
Note: Ensure you have carried out the pre-requisites as described in the Preparation section.
Steps
| 1. | Select the  tab on the WS-Engineer View |
Click on the 
button to select the WS-BPEL process, alternatively you can "drag and drop" the .bpel file on the Design View as shown below.
If the WS-BPEL file is valid, then the name of the BPEL process is shown under the 1. Process Source section.
Click on the 
button to select the Design (MSC) specification, alternatively you can "drag and drop" the .xml file on the Design View as shown below.
If the Design file is valid, then "MSC Specification Loaded" is shown under the 2. Design Source section.
Click the 
button select the source property for verification.
| • | Property as Process uses the WS-BPEL implementation as a property against the design specification (e.g. does the implementation fulfill the behaviour specified in the design specification). |
| • | Property as Specification uses the MSC Design Specification as a property against the WS-BPEL implementation (e.g. does the specification exhibit any additional behaviour not specified in the implementation). |
When both implementation and specification files are correctly loaded, the 
button will be enabled. Click the button to start the verification. If the button is not enabled after adding both valid process and design files, then it is possible that the behaviour mappings between these are not complete and must be manually assigned.
If there is behaviour found that is not equivalent (a property violation) then the point at which the violation occurs is shown as a warning.
You can click the 
button to show the trace to violation as an MSC.
If the implementation and specification are equivalent (according to the property selected) then No Violations found will be shown.
END OF TUTORIAL