A formal verification approach of conversations in composite web services

Web service composition is nowadays a very focused-on topic of research by academic and industrial research groups. This thesis discusses the design and verification of behaviors of composite web services. To model composite web services, two behaviors are proposed, namely control and operational. The operational behavior shows the business logic of the process functionality for a composite web service. The control behavior shows the constraints that the operational behavior should satisfy and specifies the states that this behavior should be in. The idea behind this separation is to promote the design, verification and reusability of web services in composite settings. To guarantee their compatibility, these two behaviors communicate and synchronize through conversation messages. State charts are used to model composite web services and symbolic model checking with NuSMV model checker is used to verify their conversations. The properties to be verified are expressed in two logics: Linear Temporal Logic (LTL) and Computation Tree Logic (CTL). A Java-based translation procedure from the design model to SMV program used by NuSMV has been developed and tested in two case studies.