BPEL4WS Verification Environment Using an Enhanced OWL-S and VDM++

This paper presents a web service verification environment to assist developers with verifying BPEL4WS documents. This environment translates a BPEL4WS document into a VDM++ document through an intermediate language called the enhanced OWL-S, and then verifies the VDM++ document by using the VDM++ toolbox. The environment is expected: 1) to provide a visual user interface of the enhanced OWL-S document for developers to quickly understand data and workflow of composite web services described in BPEL4WS, and 2) to detect consistency of data type and operation in the web service, and deadlocks in the workflow of the BPEL4WS document.