Sciweavers

Share
ICSOC
2007
Springer

Verifying Temporal and Epistemic Properties of Web Service Compositions

9 years 1 months ago
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.
Alessio Lomuscio, Hongyang Qu, Marek J. Sergot, Mo
Added 08 Jun 2010
Updated 08 Jun 2010
Type Conference
Year 2007
Where ICSOC
Authors Alessio Lomuscio, Hongyang Qu, Marek J. Sergot, Monika Solanki
Comments (0)
books