The Property Based on Action Sequence and Compliance Verification for Compositional Web Service

Requirement-driven behavioral verification for web service compositions is one of important research issue for web service. Most of behavioral specifications to be checked in existed web service verification works have forms like LTL or MSC. They are temporal relation based on actions or messages in essence. Distinguish with these work, we propose the concept of 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.