We have implemented a tool called SSCC (Service Scenario-based Consistency Checker) to solve the verification problem automatically. The implementation language of the tool is Java. It takes the WS-BPEL file and UML Sequence Diagram files as input; and gives the generated Petri net model (represented in a PNML format) and verification result as output.

ActiveBPEL Engine v4.1 is used to parse WS-BPEL code. ActiveBPEL is an open-source project developed by Active Endpoints. For more information about ActiveBPEL Engine, see their website.

After specifying the input of WS-BPEL file and Rational Rose UML Sequence Diagram files, users can choose what kind of consistency checking they want to perform. Then the tool automatically transforms WS-BPEL process into Petri net model based on the simplification mechanism, and performs the specified consistency checking against the specifications. The verification result such as what paths in the Petri net is consistent with the specifications is also represented in the tool. User can also view all the files loaded and generated by the tool. A user manual is also provided (in Chinese).

Download SSCC    Download User Manual (in Chinese)

The files used in the case study can be downloaded too. The archive consists of 6 files: the loanService.bpel file is the Loan Approval Service WS-BPEL process definition taken from ActiveBPEL Engine examples (which is also taken from WS-BPEL specification), the .wsdl and .xsd is the associated WSDL and XML Schema file also taken from ActiveBPEL Engine examples. Three .mdl files for Rational Rose. They are assessorUSD.mdl, approvalUSD.mdl and replyUSD.mdl. Each of them specifies a scenario which could be used to be verified against.
  The output files contains a .bpel file which is the simplified WS-BPEL code and an .xml file which is simplified WS-BPEL Petri net.

Case study: the Loan Approval Service