Towards Verifying Contract Regulated Service Composition
Alessio R. Lomuscio, Hongyang Qu, Monika Solanki · 2008
We report on a novel approach to (semi-)automatically compile and verify contract-regulated service compositions. We specify Web services and the contracts governing them as WSBPEL behaviours. We compile WSBPEL behaviours into the specialised system description language ISPL, to be used with the model checker MCMAS to verify behaviours automatically. We use the formalism of temporal-epistemic logic suitably extended to deal with compliance/violations of contracts. We illustrate these concepts using a motivating example whose state space is approximately 106and discuss experimental results.