The tools include a capability to generate a service implementation, for a participant in a choreography, using WS-BPEL.
When a choreography description has been created, it is possible to generate a BPEL Process (and associated WSDL files and deployment descriptor) for each of the participants defined within the choreography. To try this out, select the Savara->Generate->Service menu item from the popup menu associated with the architecture/PurchaseGoods.bpmn.
This will display a dialog listing the possible services that can be generated from this choreography, with a proposed Eclipse project name, and the option to select a service type.
Press the 'Ok' button and this will create a single a BPEL project for the Store, Logistics and CreditAgency participants.
Each project will contain a single bpelContent folder containing the WS-BPEL process definition for the participant, a list of relevant WSDL files and a deployment descriptor file for use with any Apache ODE based engine (e.g. RiftSaw). However the WS-BPEL and WSDL files are standard, so can be deployed to any WS-BPEL 2.0 compliant engine.
The SAVARA tools include the ability to statically verify the external observable behaviour of a BPEL process definition against other artifacts (e.g. a scenario).
To verify a scenario against one or more BPEL process definitions, open the scenario in the editor and select the green play button. When the dialog is displayed, select the BPEL process associated with the role being simulated. For example, the Store role should be associated with the generated PurchaseGoods_Store.bpel, the CreditAgency role associated with the PurchaseGoods_CreditAgency.bpel, etc. When the OK button is pressed, the simulation will be performed against the selected BPEL process definitions.
'Static' verification refers to the fact that a protocol description is derived from the BPEL process, describing the communications behaviour of the process. It is this protocol description that is validated against other artifacts - in this case a scenario.
In contract, a dynamic verification would involve actually executing an instance of the BPEL process, to determine whether it correctly behaves when presented with a series of sample (simulated) use cases. We hope to be able to support this functionality in the near future.