Research On The Methods For Detecting Mismatch Of Web Services Based On Bounded Model Checking

As a new paradigm of software development, Service Oriented Architecture(SOA) is gradually becoming one of the future software development trends. As the mainstream realization of SOA, Web service technology has also obtained rapid development and application. The single Web service is often unable to meet the individual requirements, so multiple services needs to be assembled into a more valuable and larger size services or systems to meet the complex requirements. However, due to inconsistence of the interface type, data format or interaction protocol, services can not be combined in the right way. Web services mismatch detection can accurately capture the mismatch points, which creates a foundation for realizing right interaction.From the perspective of interoperability levels, service mismatch may occur in the signature, behavioral, semantic and other levels. Among them, the mismatch of behavioral level is critical and difficult. This paper only researches the mismatch of the behavioral layer. If every service eventually reaches their final state after interaction there is no mismatch, or exists mismatch. In other words, this paper transforms the mismatch detection problem into the compatibility determination issues.Formal verification techniques(such as model checking), one of the important methods to ensure the quality of the software, now is widely used in Web service verification. Bounded model checking(BMC) uses the progressive detection from local to global, which can find counterexamples rapidly. This paper studys Web services mismatch detection using BMC. The major works are summarized as follows: (1) A method is proposed for detecting mismatch of Web services based on NuSMV. Given Web service behavior and the formal description of compatibility at first, and then use the model checking tool NuSMV which supports BMC to verify whether service interaction model satisfies the compatibility or not. The tool will give counterexample when the model doesn't meet the property. (2) A method is proposed for detecting mismatch of Web services based on SMT. It determines the compatibility of Web services interactions through checking whether there exists deadlock during the service interaction process. The method first models the interaction behavior of Web service, and then converted the model and compatibility to the logical formula which can be accepted by SMT tools. Finally SMT is used to achieve mismatch detection. (3) The paper brings timed properties into Web services interaction, creates formal model for Web service with time property and proposes a method for detecting mismatch of time-aware Web services based on SMT.