A Novel Method for Verification of Composite Web Services

This paper presents a novel method based on object-oriented MSVL for verification of composite Web services described by OWL-S. First, object-oriented MSVL, an executable temporal logic language for modelling, is briefly presented. Secondly, modelling rules are defined for OWL-S which is used to compose Web services. Further, Propositional Projection Temporal Logic (PPTL), a specification language for describing desirable properties, is presented and the verification method is proposed. At last, the verification method is illustrated by a bookstore example based on Web services.