In this tutorial the user will be able to model-check that WS-BPEL orchestrations are "safe" given their behaviour and resource constraints specified in a deployment architecture configuration.
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. |
| 2. | Select the Deployment Specification File |
Click on the 
button to select a Deployment Model Package, alternatively you can "drag and drop" the a XADL2.0 xml file or UML2.0 XMI file on the Deployment View as shown below.
| 3. | Select the Deployment Model |
Expanding the Model list aside the Architecture Model will list all available models in the deployment model package.
Note: The default model is the first model found in the package.
4. Select the WS-BPEL and WSDL process pairs to analyse
Drag and drop selected WS-BPEL and WSDL files (together) in the Process Source list box of the deployment view. Repeat this for as many interacting processes as you wish to analyse.
Note: Each WS-BPEL process is paired with one or more WSDL files. In this sample, we associate one WS-BPEL with one WSDL file.
When both deployment model and WS-BPEL files are correctly loaded, the 
button will be enabled. Click the button to start the verification.
If there is a violation of the behaviour specified in the WS-BPEL and the deployment configuration resources 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 there are no violations found then No Violations found will be shown.
6. Repeat the Verify action for alternative deployment models
END OF TUTORIAL