The Binary Behavioral Modes Based on Action Sequence and Compliance Verification for Compositional Web Service

To verify whether a compositional Web service is compliant to the specific requirements of users is one of important research issue for Web service. Most of existed work about Web service verification do not address the issue of how to model the requirements that the BPEL4WS processes are supposed to satisfy. The specifications are temporal relation based on actions or messages in essence. Distinguish with these work, we propose the concept of binary behavioral specification based on action sequence. Express these specifications as behavioral modes. Encode them on LTS and then give them operation semantics. After modeling compositional Web services as LTS, sufficient and necessary conditions and algorithms have been given for checking them whether the given Web service compositions compliant to the behavioral mode.