Agreement and Compensation Verification in Long-running Transactions

Abstract

This paper presents formal analysis of an application example that makes use of long-running, nested, and compensation-based services which require coordination and agreement in order to perform a joint business task. The communication is supported with the use of Web Services Business Activity protocol suitable for implementation of complex business processes. The main contributions of the paper include the analysis of the suitability of the business activity protocol in order to be used in complex services that the designers claim this protocol is developed for. Furthermore, the paper proposes a separation of compensation logic from the protocol about which the protocol specification is not clear. Analysis is performed using the model-checker UPPAAL and the property of main interest is to verify the consistent outcome of the business process once the services complete their work.