SPIN Based Verification Of Service Composition and Compensation

Abstract

In a web service, there occur business transactions. Sometimes there may occur some sorts of difficulties in the terms of transactions. To provide a good web service, it’s composition needs to get verified and those difficulties need to get handled. And so our motivation is to verify composition and compensation of the web service. We have used car broker web service as our composition to verify and compensate the web service to provide a good web service. And so we have composed and compensated this service and verified this through the LTL verifications using PROMELA language in SPIN tool.