Towards verifying contract regulated service composition

Abstract 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 10 6 and discuss experimental results.

Authors

• Alessio Lomuscio Imperial College London
• Hongyang Qu
• Monika Solanki

Keywords

• Multi-agent systems
• Web services
• Model checking