Verification of Web Service Composition Using “SPIN”

Abstract

Web service composition and its verification is an important part to get an error free web service. In a web service there are huge business transaction occurs. Sometimes in business transaction, it needs to deal with faults that can arise in any stage of transaction. So always roll back mechanism is not possible to solve this problem. In order to achieve a common business goal, the protocol of interaction must be correct. In this project we have established a Broker system and encode this overall model into PROMELA (Model checking Language). For verify this model we also have used linear temporal logic and convert it to never claim property to verify this model accuracy. If any oversight happened then a compensation mechanism has been used to handle the situation.