Abstract
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. © Springer-Verlag Berlin Heidelberg 2007.
Cite
CITATION STYLE
Lomuscio, A., Qu, H., Sergot, M., & Solanki, M. (2007). Verifying temporal and epistemic properties of Web service compositions. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4749 LNCS, pp. 456–461). Springer Verlag. https://doi.org/10.1007/978-3-540-74974-5_43
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
