Towards verifying contract regulated service composition

摘要

We report on a novel approach to (semi-)automatically compile and verify contract-regulated service compositions implemented as multi-agent systems. We model web service behaviours and the contracts governing them as WSBPEL specification. We use the formalism of temporal-epistemic logic, suitably extended to deal with compliance/violations of contracts, to specify properties of service compositions. We compile the WSBPEL behaviours into a specialised system description language ISPL, to be used with the model checker MCMAS to verify the behaviours automatically. We illustrate these concepts using a motivating example whose state space is approximately 106 and discuss experimental results.