A Composition Compensation Mechanism Based Paired Net and Verification

With regard to the failure and cancellation of business logic of Web services composition, we present a composition compensation mechanism based on paired net to implement partial or full compensation of the committed activities. The introduction of this method can accurately construct SCPN and establish agile compensation-triggered mechanism which can satisfy prospective compensation requirements, meaning either successfully committed, or effects of completed activities eliminated. We also verify the significant properties of the compensation paired net system, such as the reachability, liveness and deadlock- freeness, and thus ensure that the composition compensation method based on paired net is feasible.