Choreography Conformance Analysis: Asynchronous Communications and Information Alignment

Web service choreography languages provide a way to describe the collaboration protocol of multiple services that exchange information in order to achieve a common goal. This description may be seen as a specification that should be respected by the joint behavior of the set of services implementing the choreography. Such a conformance requires that (i) the observable behavior of the implementation corresponds to the behavior described by the protocol specification, and (ii) the business information is properly managed, guaranteeing that the participants have a shared knowledge about it, according to what is specified in the choreography. In this paper we present a choreography conformance analysis approach that addresses both the behavioral correspondence and the business information management. The key features of the approach are the capability to deal with asynchronous interactions and the ability to model and analyse the data managed and exchanged in the protocol, thus providing more accurate verification results. We also present symbolic techniques based on these formalizations that can be used for model checking of the choreography conformance.