University of Lueneburg
The increasing diffusion of service oriented computing in critical business transactions demands reliability and correctness of the workflow logic representing web service orchestrations. The authors present an approach for the formal verification of workflow-based compositions of web services, described in BPEL4WS. Workflow processes can be verified in isolation, assuming that the external services invoked are known only through their interface. It is also possible to verify that the actual composition of two or more processes behaves correctly. They can verify deadlock freedom, properties expressed as data-bound assertions written in WS-CoL, a specification language for web services, and LTL temporal properties.