is a formal approach of verifying non-functional properties for web
services orchestrations. Two classes of properties have to be taken into
account: generic and specific properties. Generic properties can be
verified for any web service involved in a given orchestration.
Specific properties are the dependent relations between activities for
a given BPEL process.
To do this, we have developed a tool which takes
a web service orchestration specified with BPEL 2.0 as an input and a
set of properties and returns the verification result as an output. The
verification is achieved by using the SPIN model-checker. The
transformation from BPEL to Promela, the input language for SPIN, is fullfilled with the use of ANTLR tool (ANother Tool for Language Recognition).