We report on a novel approach to (semi-)automatically compile and verify contract-regulated service compositions. We specify webservices 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 10^6 and discuss experimental results.
展开▼
