A question of Composite Web Service Verification

Dear Colleagues,

    I am a new comer of the area of Web Service. In recent study, I met with a problem of how to verify that the structure of web service compostion is well-formed. Can I say a structure is well-formed if the structure satisfies the following properties: reachability and deadlock-freedom? (Reachability means that all the services included in the Composition can be reached while excuting the composition)  And if it is, how to verify the structure used to composite web services is well-formed?

Thanks

 
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Jianchao Wang
Technology Center of Software Engineering
Institute of Software, Chinese Academy of Sciences
P.O.Box 8718, Beijing 100080, P.R.China
Email: jcwang@otcaix.iscas.ac.cn
Phone: +8610-62630989-203
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~