BPELVT 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).