Formal verification for Web service composition: A model-checking approach

Formal methods are an effective way for modeling and verifying concurrent systems. In this paper, labeled transition systems are proposed as an approach to deal with the modeling of the composition of Web services. The presented model represents a Web service as a couple consisting of a representation of the Web service and a set of its states. We argue that notions that have been used in the modeling of compound Web services including Petri nets and process calculus can be described in the same formal framework namely labeled transition systems. We use the model-checking approach in order to verify this composition and a set of properties written in temporal logic. Unlike previous work, our approach allows to model and verify not only the composition of Web services, but also the internal activities for each invocated service. Finally, a case study is carried out and the validity of a compound Web service is verified.