Verifying Temporal and Epistemic Properties of Web Service Compositions

Model checking Web service behaviour has remained limited to checking safety and liveness properties. However when viewed as a multi agent system, the system composition can be analysed by considering additional properties which capture the knowledge acquired by services during their interactions. In this paper we present a novel approach to model checking service composition where in addition to safety and liveness, epistemic properties are analysed and verified. To do this we use a specialised system description language (ISPL) paired with a symbolic model checker (MCMAS) optimised for the verification of temporal and epistemic modalities. We report on experimental results obtained by analysing the composition for a Loan Approval Service.

• Type: Conference
• Year: 2007
• Where: ICSOC
• Authors: Alessio Lomuscio, Hongyang Qu, Marek J. Sergot, Monika Solanki
• Keywords: ICSOC 2007, Model Checking, Model Checking Web, Multi Agent System