Verifying conformance between Web service choreography and implementation using learning and model checking

摘要

A conformance problem between Web service choreography and orchestration has attracted much interest in the research field of Web service composition. A number of formal languages have been proposed for describing both choreography and orchestration. Moreover, various notions of conformance between them have been formally defined. In most of the earlier works, however, it is assumed that the internal structures of implemented orchestration are explicit. It may not always be the case, such as the Web services implemented in. NET or Java. In this paper, we have investigated an alternative approach for verifying a conformance between choreography and the implementation whose only external behavior can be observed. We use an adapted version of Angluin's algorithm to infer a Mealy machine from the implemented Web service. By transforming the Mealy machine to the modeling formalism LTS, the model checker LTSA can be used for checking the conformance criterion in our framework.